changeset 74337 | 9c1ad2f04660 |
parent 74334 | ead56ad40e15 |
child 76224 | 64e8d4afcf10 |
74336:7bb0ac635397 | 74337:9c1ad2f04660 |
---|---|
102 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
102 "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10) |
103 |
103 |
104 end |
104 end |
105 |
105 |
106 unbundle no_lattice_syntax |
106 unbundle no_lattice_syntax |
107 no_notation Inf ("\<Sqinter>") and Sup ("\<Squnion>") |
|
108 |
107 |
109 end |
108 end |