--- a/src/HOL/BNF/BNF.thy Thu Jan 16 20:52:54 2014 +0100
+++ b/src/HOL/BNF/BNF.thy Thu Jan 16 21:22:01 2014 +0100
@@ -15,6 +15,6 @@
hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr
convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
- prefCl PrefCl Succ Shift shift
+ prefCl PrefCl Succ Shift shift proj
end
--- a/src/HOL/BNF/BNF_GFP.thy Thu Jan 16 20:52:54 2014 +0100
+++ b/src/HOL/BNF/BNF_GFP.thy Thu Jan 16 21:22:01 2014 +0100
@@ -15,6 +15,10 @@
"primcorec" :: thy_decl
begin
+setup {*
+Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
+*}
+
lemma not_TrueE: "\<not> True \<Longrightarrow> P"
by (erule notE, rule TrueI)
--- a/src/HOL/Equiv_Relations.thy Thu Jan 16 20:52:54 2014 +0100
+++ b/src/HOL/Equiv_Relations.thy Thu Jan 16 21:22:01 2014 +0100
@@ -497,5 +497,6 @@
"equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
by (erule equivpE, erule transpE)
+hide_const (open) proj
+
end
-