--- a/src/HOL/Lfp.ML Wed May 15 13:51:15 1996 +0200
+++ b/src/HOL/Lfp.ML Fri May 17 12:23:44 1996 +0200
@@ -51,16 +51,10 @@
rtac (CollectI RS subsetI), rtac indhyp, atac]);
qed "induct";
-val major::prems = goal Lfp.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);
-by (rtac (major RS induct) 1);
-by (resolve_tac prems 1);
-by (res_inst_tac[("p","x")]PairE 1);
-by (hyp_subst_tac 1);
-by (asm_simp_tac (!simpset addsimps prems) 1);
-qed"induct2";
+bind_thm
+ ("induct2",
+ Prod_Syntax.split_rule
+ (read_instantiate [("a","(a,b)")] induct));
(*** Fixpoint induction a la David Park ***)
goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A";