src/FOL/ex/NewLocaleTest.thy

--- a/src/FOL/ex/NewLocaleTest.thy	Mon Dec 08 14:22:42 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Mon Dec 08 18:44:24 2008 +0100
@@ -121,9 +121,14 @@
     and lnot ("-- _" [60] 60)
   assumes assoc: "(x && y) && z = x && (y && z)"
     and notnot: "-- (-- x) = x"
-  defines "x || y == --(-- x && -- y)"
+  defines lor_def: (* FIXME *) "x || y == --(-- x && -- y)"
+begin
 
-print_locale! logic_def
+lemma "x || y = --(-- x && --y)"
+  by (unfold lor_def) (rule refl)
+
+end
+
 
 text {* Theorem statements *}