# HG changeset patch
# User haftmann
# Date 1470848240 -7200
# Node ID 92e0378036662d62903227293063e23d6e2e0f87
# Parent  76302202a92d7fe0cc0e023fdd668f4b4213ba6a
formal passive interpretation proofs for conj and disj

diff -r 76302202a92d -r 92e037803666 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>