Moved induct2 from Hoare to Lfp.

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