hide short const name
authorblanchet
Thu Jan 16 21:22:01 2014 +0100 (2014-01-16)
changeset 5502405cc0dbf3a50
parent 55023 38db7814481d
child 55025 1ac0a0194428
hide short const name
src/HOL/BNF/BNF.thy
src/HOL/BNF/BNF_GFP.thy
src/HOL/Equiv_Relations.thy
     1.1 --- a/src/HOL/BNF/BNF.thy	Thu Jan 16 20:52:54 2014 +0100
     1.2 +++ b/src/HOL/BNF/BNF.thy	Thu Jan 16 21:22:01 2014 +0100
     1.3 @@ -15,6 +15,6 @@
     1.4  
     1.5  hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
     1.6    convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
     1.7 -  prefCl PrefCl Succ Shift shift
     1.8 +  prefCl PrefCl Succ Shift shift proj
     1.9  
    1.10  end
     2.1 --- a/src/HOL/BNF/BNF_GFP.thy	Thu Jan 16 20:52:54 2014 +0100
     2.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Thu Jan 16 21:22:01 2014 +0100
     2.3 @@ -15,6 +15,10 @@
     2.4    "primcorec" :: thy_decl
     2.5  begin
     2.6  
     2.7 +setup {*
     2.8 +Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
     2.9 +*}
    2.10 +
    2.11  lemma not_TrueE: "\<not> True \<Longrightarrow> P"
    2.12  by (erule notE, rule TrueI)
    2.13  
     3.1 --- a/src/HOL/Equiv_Relations.thy	Thu Jan 16 20:52:54 2014 +0100
     3.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Jan 16 21:22:01 2014 +0100
     3.3 @@ -497,5 +497,6 @@
     3.4    "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
     3.5    by (erule equivpE, erule transpE)
     3.6  
     3.7 +hide_const (open) proj
     3.8 +
     3.9  end
    3.10 -