src/HOL/BNF_Greatest_Fixpoint.thy
changeset 66248 df85956228c2
parent 64413 c0d5e78eb647
child 67091 1393c2340eec
     1.1 --- a/src/HOL/BNF_Greatest_Fixpoint.thy	Mon Jul 03 09:57:26 2017 +0200
     1.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Mon Jul 03 13:51:55 2017 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    "primcorec" :: thy_decl
     1.5  begin
     1.6  
     1.7 -setup \<open>Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}\<close>
     1.8 +alias proj = Equiv_Relations.proj
     1.9  
    1.10  lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    1.11    by simp