src/HOL/Main.thy
changeset 55087 252c7fec4119
parent 55086 500ef036117b
child 55128 6e16d2dd4f14
     1.1 --- a/src/HOL/Main.thy	Mon Jan 20 21:45:08 2014 +0100
     1.2 +++ b/src/HOL/Main.thy	Mon Jan 20 22:24:48 2014 +0100
     1.3 @@ -11,11 +11,6 @@
     1.4  
     1.5  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
     1.6  
     1.7 -hide_const (open)
     1.8 -  image2 image2p vimage2p Gr Grp collect fsts snds setl setr
     1.9 -  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
    1.10 -  prefCl PrefCl Succ Shift shift proj
    1.11 -
    1.12  no_notation
    1.13    bot ("\<bottom>") and
    1.14    top ("\<top>") and
    1.15 @@ -33,6 +28,11 @@
    1.16    cexp (infixr "^c" 90) and
    1.17    convol ("<_ , _>")
    1.18  
    1.19 +hide_const (open)
    1.20 +  image2 image2p vimage2p Gr Grp collect fsts snds setl setr
    1.21 +  convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
    1.22 +  prefCl PrefCl Succ Shift shift proj
    1.23 +
    1.24  no_syntax (xsymbols)
    1.25    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    1.26    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)