--- a/src/FOL/ex/NewLocaleTest.thy Fri Dec 05 16:41:36 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy Mon Dec 08 14:18:29 2008 +0100
@@ -113,6 +113,18 @@
print_locale! use_decl thm use_decl_def
+text {* Defines *}
+
+locale logic_def =
+ fixes land (infixl "&&" 55)
+ and lor (infixl "||" 50)
+ and lnot ("-- _" [60] 60)
+ assumes assoc: "(x && y) && z = x && (y && z)"
+ and notnot: "-- (-- x) = x"
+ defines "x || y == --(-- x && -- y)"
+
+print_locale! logic_def
+
text {* Theorem statements *}
lemma (in lgrp) lcancel: