diff -r 0ea94f540548 -r e74341997a48 src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Tue Dec 09 15:34:49 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Tue Dec 09 21:27:00 2008 +0100
@@ -130,11 +130,23 @@
   defines "x || y == --(-- x && -- y)"
 begin
 
+thm lor_def
+(* Can we get rid the the additional hypothesis, caused by LocalTheory.notes? *)
+
 lemma "x || y = --(-- x && --y)"
   by (unfold lor_def) (rule refl)
 
 end
 
+(* Inheritance of defines *)
+
+locale logic_def2 = logic_def
+begin
+
+lemma "x || y = --(-- x && --y)"
+  by (unfold lor_def) (rule refl)
+
+end
 
 text {* Theorem statements *}