src/HOL/BNF_Greatest_Fixpoint.thy
changeset 58826 2ed2eaabe3df
parent 58352 37745650a3f4
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Wed Oct 29 17:01:44 2014 +0100
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Wed Oct 29 19:01:49 2014 +0100
     1.3 @@ -17,9 +17,7 @@
     1.4    "primcorec" :: thy_decl
     1.5  begin
     1.6  
     1.7 -setup {*
     1.8 -Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
     1.9 -*}
    1.10 +setup {* Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj} *}
    1.11  
    1.12  lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.13    by simp