--- 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 *}