src/HOLCF/Fixrec.thy
changeset 40327 1dfdbd66093a
parent 40322 707eb30e8a53
child 40502 8e92772bc0e8
     1.1 --- a/src/HOLCF/Fixrec.thy	Fri Oct 29 16:51:40 2010 -0700
     1.2 +++ b/src/HOLCF/Fixrec.thy	Fri Oct 29 17:15:28 2010 -0700
     1.3 @@ -222,11 +222,11 @@
     1.4  by simp
     1.5  
     1.6  lemma def_cont_fix_eq:
     1.7 -  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_CFun F); cont F\<rbrakk> \<Longrightarrow> f = F f"
     1.8 +  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F\<rbrakk> \<Longrightarrow> f = F f"
     1.9  by (simp, subst fix_eq, simp)
    1.10  
    1.11  lemma def_cont_fix_ind:
    1.12 -  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_CFun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
    1.13 +  "\<lbrakk>f \<equiv> fix\<cdot>(Abs_cfun F); cont F; adm P; P \<bottom>; \<And>x. P x \<Longrightarrow> P (F x)\<rbrakk> \<Longrightarrow> P f"
    1.14  by (simp add: fix_ind)
    1.15  
    1.16  text {* lemma for proving rewrite rules *}