equal
deleted
inserted
replaced
68 |
68 |
69 val prems = goal (the_context ()) |
69 val prems = goal (the_context ()) |
70 " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \ |
70 " [| x:lfp(f); mono(f); !!y. y:f(lfp(f) Int {x. P(x)}) ==> P(y) |] ==> \ |
71 \ P(x)"; |
71 \ P(x)"; |
72 by (cut_facts_tac prems 1); |
72 by (cut_facts_tac prems 1); |
73 by (etac lfp_induct 1); |
73 by (etac (thm "lfp_induct_set") 1); |
74 by (assume_tac 1); |
74 by (assume_tac 1); |
75 by (eresolve_tac prems 1); |
75 by (eresolve_tac prems 1); |
76 qed "lfp_ind2"; |
76 qed "lfp_ind2"; |
77 |
77 |
78 (* Greatest fixpoints *) |
78 (* Greatest fixpoints *) |