src/HOL/Lattices.thy

--- a/src/HOL/Lattices.thy	Mon Aug 08 14:01:49 2016 +0200
+++ b/src/HOL/Lattices.thy	Wed Aug 10 18:57:20 2016 +0200
@@ -139,6 +139,16 @@
 
 end
 
+text \<open>Passive interpretations for boolean operators\<close>
+
+lemma semilattice_neutr_and:
+  "semilattice_neutr HOL.conj True"
+  by standard auto
+
+lemma semilattice_neutr_or:
+  "semilattice_neutr HOL.disj False"
+  by standard auto
+
 
 subsection \<open>Syntactic infimum and supremum operations\<close>