equal
deleted
inserted
replaced
28 cprod (infixr "*c" 80) and |
28 cprod (infixr "*c" 80) and |
29 cexp (infixr "^c" 90) and |
29 cexp (infixr "^c" 90) and |
30 convol ("\<langle>(_,/ _)\<rangle>") |
30 convol ("\<langle>(_,/ _)\<rangle>") |
31 |
31 |
32 hide_const (open) |
32 hide_const (open) |
33 czero cinfinite cfinite csum cone ctwo Csum cprod cexp |
33 czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect |
34 image2 image2p vimage2p Gr Grp collect fsts snds setl setr |
34 fsts snds setl setr convol pick_middlep fstOp sndOp csquare relImage relInvImage Succ Shift |
35 convol pick_middlep fstOp sndOp csquare relImage relInvImage |
35 shift proj |
36 Succ Shift shift proj |
|
37 |
36 |
38 no_syntax (xsymbols) |
37 no_syntax (xsymbols) |
39 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
38 "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_./ _)" [0, 10] 10) |
40 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
39 "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10) |
41 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |
40 "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10) |