| changeset 33837 | a406f447abef |
| parent 33836 | da3e88ea6c72 |
| child 36089 | 8078d496582c |
--- a/src/FOL/ex/LocaleTest.thy Sat Nov 21 17:37:07 2009 +0100 +++ b/src/FOL/ex/LocaleTest.thy Sat Nov 21 17:39:54 2009 +0100 @@ -195,7 +195,6 @@ begin thm lor_def -(* Can we get rid the the additional hypothesis, caused by Local_Theory.notes? *) lemma "x || y = --(-- x && --y)" by (unfold lor_def) (rule refl)