moved hide_const from BNF to Main
authorblanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55069b3e44be90122
parent 55068 526671cca4a7
child 55070 235c7661a96b
moved hide_const from BNF to Main
src/HOL/BNF/BNF.thy
src/HOL/Main.thy
     1.1 --- a/src/HOL/BNF/BNF.thy	Mon Jan 20 18:24:56 2014 +0100
     1.2 +++ b/src/HOL/BNF/BNF.thy	Mon Jan 20 18:24:56 2014 +0100
     1.3 @@ -13,8 +13,4 @@
     1.4  imports Countable_Set_Type BNF_Decl
     1.5  begin
     1.6  
     1.7 -hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
     1.8 -  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
     1.9 -  prefCl PrefCl Succ Shift shift proj
    1.10 -
    1.11  end
     2.1 --- a/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
     2.2 +++ b/src/HOL/Main.thy	Mon Jan 20 18:24:56 2014 +0100
     2.3 @@ -11,6 +11,11 @@
     2.4  
     2.5  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
     2.6  
     2.7 +hide_const (open)
     2.8 +  image2 image2p vimage2p Gr Grp collect fsts snds setl setr
     2.9 +  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
    2.10 +  prefCl PrefCl Succ Shift shift proj
    2.11 +
    2.12  no_notation
    2.13    bot ("\<bottom>") and
    2.14    top ("\<top>") and