1.1 --- a/src/HOL/IMP/Hoare.ML	Tue May 09 22:10:08 1995 +0200
     1.2 +++ b/src/HOL/IMP/Hoare.ML	Tue May 09 22:10:48 1995 +0200
     1.3 @@ -38,17 +38,6 @@
     1.4  by(fast_tac comp_cs 1);
     1.5  qed"hoare_if";
     1.6  
     1.7 -val major::prems = goal Hoare.thy
     1.8 -  "[| (a,b) :lfp f; mono f; \
     1.9 -\     !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
    1.10 -by(res_inst_tac [("c1","P")] (split RS subst) 1);
    1.11 -br (major RS induct) 1;
    1.12 -brs prems 1;
    1.13 -by(res_inst_tac[("p","x")]PairE 1);
    1.14 -by(hyp_subst_tac 1);
    1.15 -by(asm_simp_tac (prod_ss addsimps prems) 1);
    1.16 -qed"induct2";
    1.17 -
    1.18  goalw Hoare.thy (spec_def::C_simps)
    1.19    "!!P. [| {{%s. P s & B b s}} c {{P}} |] ==> \
    1.20  \  {{P}} while b do c {{%s. P s & ~B b s}}";