src/HOL/Inductive.thy
changeset 46008 c296c75f4cf4
parent 45907 4b41967bd77e
child 46947 b8c7eb0c2f89
     1.1 --- a/src/HOL/Inductive.thy	Wed Dec 28 15:08:12 2011 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Wed Dec 28 20:03:13 2011 +0100
     1.3 @@ -108,7 +108,7 @@
     1.4    and P_f: "!!S. P S ==> P(f S)"
     1.5    and P_Union: "!!M. !S:M. P S ==> P(Union M)"
     1.6    shows "P(lfp f)"
     1.7 -  using assms by (rule lfp_ordinal_induct [where P=P])
     1.8 +  using assms by (rule lfp_ordinal_induct)
     1.9  
    1.10  
    1.11  text{*Definition forms of @{text lfp_unfold} and @{text lfp_induct}, 
    1.12 @@ -210,7 +210,7 @@
    1.13  apply (rule Un_least [THEN Un_least])
    1.14  apply (rule subset_refl, assumption)
    1.15  apply (rule gfp_unfold [THEN equalityD1, THEN subset_trans], assumption)
    1.16 -apply (rule monoD [where f=f], assumption)
    1.17 +apply (rule monoD, assumption)
    1.18  apply (subst coinduct3_mono_lemma [THEN lfp_unfold], auto)
    1.19  done
    1.20