--- a/src/HOL/Inductive.thy Mon Dec 28 16:34:26 2015 +0100
+++ b/src/HOL/Inductive.thy Mon Dec 28 17:43:30 2015 +0100
@@ -87,16 +87,16 @@
lemma lfp_induct_set:
assumes lfp: "a: lfp(f)"
- and mono: "mono(f)"
- and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
+ and mono: "mono(f)"
+ and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
shows "P(a)"
by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
(auto simp: intro: indhyp)
lemma lfp_ordinal_induct_set:
assumes mono: "mono f"
- and P_f: "!!S. P S ==> P(f S)"
- and P_Union: "!!M. !S:M. P S ==> P(Union M)"
+ and P_f: "!!S. P S ==> P(f S)"
+ and P_Union: "!!M. !S:M. P S ==> P (\<Union>M)"
shows "P(lfp f)"
using assms by (rule lfp_ordinal_induct)