equal
deleted
inserted
replaced
137 sublocale ordering_top less_eq less "\<^bold>1" |
137 sublocale ordering_top less_eq less "\<^bold>1" |
138 by standard (simp add: order_iff) |
138 by standard (simp add: order_iff) |
139 |
139 |
140 end |
140 end |
141 |
141 |
|
142 text \<open>Passive interpretations for boolean operators\<close> |
|
143 |
|
144 lemma semilattice_neutr_and: |
|
145 "semilattice_neutr HOL.conj True" |
|
146 by standard auto |
|
147 |
|
148 lemma semilattice_neutr_or: |
|
149 "semilattice_neutr HOL.disj False" |
|
150 by standard auto |
|
151 |
142 |
152 |
143 subsection \<open>Syntactic infimum and supremum operations\<close> |
153 subsection \<open>Syntactic infimum and supremum operations\<close> |
144 |
154 |
145 class inf = |
155 class inf = |
146 fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |
156 fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70) |