moved hide_const from BNF to Main
authorblanchet
Mon, 20 Jan 2014 18:24:56 +0100
changeset 55069 b3e44be90122
parent 55068 526671cca4a7
child 55070 235c7661a96b
moved hide_const from BNF to Main
src/HOL/BNF/BNF.thy
src/HOL/Main.thy
--- a/src/HOL/BNF/BNF.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/BNF/BNF.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -13,8 +13,4 @@
 imports Countable_Set_Type BNF_Decl
 begin
 
-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 proj
-
 end
--- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
+++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
@@ -11,6 +11,11 @@
 
 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
 
+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 proj
+
 no_notation
   bot ("\<bottom>") and
   top ("\<top>") and