src/HOL/BNF/BNF_GFP.thy
changeset 55024 05cc0dbf3a50
parent 55022 eeba3ba73486
     1.1 --- a/src/HOL/BNF/BNF_GFP.thy	Thu Jan 16 20:52:54 2014 +0100
     1.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Thu Jan 16 21:22:01 2014 +0100
     1.3 @@ -15,6 +15,10 @@
     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 +
    1.11  lemma not_TrueE: "\<not> True \<Longrightarrow> P"
    1.12  by (erule notE, rule TrueI)
    1.13