src/HOL/Main.thy
changeset 58152 6fe60a9a5bad
parent 58128 43a1ba26a8cb
child 58154 47c3c7019b97
     1.1 --- a/src/HOL/Main.thy	Wed Sep 03 00:06:23 2014 +0200
     1.2 +++ b/src/HOL/Main.thy	Wed Sep 03 00:06:24 2014 +0200
     1.3 @@ -30,10 +30,9 @@
     1.4    convol ("\<langle>(_,/ _)\<rangle>")
     1.5  
     1.6  hide_const (open)
     1.7 -  czero cinfinite cfinite csum cone ctwo Csum cprod cexp
     1.8 -  image2 image2p vimage2p Gr Grp collect fsts snds setl setr
     1.9 -  convol pick_middlep fstOp sndOp csquare relImage relInvImage
    1.10 -  Succ Shift shift proj
    1.11 +  czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
    1.12 +  fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift
    1.13 +  shift proj
    1.14  
    1.15  no_syntax (xsymbols)
    1.16    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)