src/HOL/Inductive.thy
changeset 61952 546958347e05
parent 61799 4cf66f21b764
child 61955 e96292f32c3c
     1.1 --- a/src/HOL/Inductive.thy	Mon Dec 28 16:34:26 2015 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Mon Dec 28 17:43:30 2015 +0100
     1.3 @@ -87,16 +87,16 @@
     1.4  
     1.5  lemma lfp_induct_set:
     1.6    assumes lfp: "a: lfp(f)"
     1.7 -      and mono: "mono(f)"
     1.8 -      and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
     1.9 +    and mono: "mono(f)"
    1.10 +    and indhyp: "!!x. [| x: f(lfp(f) Int {x. P(x)}) |] ==> P(x)"
    1.11    shows "P(a)"
    1.12    by (rule lfp_induct [THEN subsetD, THEN CollectD, OF mono _ lfp])
    1.13       (auto simp: intro: indhyp)
    1.14  
    1.15  lemma lfp_ordinal_induct_set: 
    1.16    assumes mono: "mono f"
    1.17 -  and P_f: "!!S. P S ==> P(f S)"
    1.18 -  and P_Union: "!!M. !S:M. P S ==> P(Union M)"
    1.19 +    and P_f: "!!S. P S ==> P(f S)"
    1.20 +    and P_Union: "!!M. !S:M. P S ==> P (\<Union>M)"
    1.21    shows "P(lfp f)"
    1.22    using assms by (rule lfp_ordinal_induct)
    1.23