src/HOL/Inductive.thy
changeset 61076 bdc1e2f0a86a
parent 60758 d8d85a8172b5
child 61337 4645502c3c64
     1.1 --- a/src/HOL/Inductive.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  subsection \<open>General induction rules for least fixed points\<close>
     1.5  
     1.6  lemma lfp_ordinal_induct[case_names mono step union]:
     1.7 -  fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
     1.8 +  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
     1.9    assumes mono: "mono f"
    1.10    and P_f: "\<And>S. P S \<Longrightarrow> S \<le> lfp f \<Longrightarrow> P (f S)"
    1.11    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Sup M)"
    1.12 @@ -177,7 +177,7 @@
    1.13    by (blast dest: gfp_lemma2 mono_Un)
    1.14  
    1.15  lemma gfp_ordinal_induct[case_names mono step union]:
    1.16 -  fixes f :: "'a\<Colon>complete_lattice \<Rightarrow> 'a"
    1.17 +  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
    1.18    assumes mono: "mono f"
    1.19    and P_f: "\<And>S. P S \<Longrightarrow> gfp f \<le> S \<Longrightarrow> P (f S)"
    1.20    and P_Union: "\<And>M. \<forall>S\<in>M. P S \<Longrightarrow> P (Inf M)"