| changeset 28936 | f1647bf418f5 |
| parent 28927 | 7e631979922f |
| child 28993 | 829e684b02ef |
--- a/src/FOL/ex/NewLocaleTest.thy Mon Dec 01 13:43:32 2008 +0100 +++ b/src/FOL/ex/NewLocaleTest.thy Mon Dec 01 16:59:31 2008 +0100 @@ -157,11 +157,6 @@ show ?t by (rule x [OF `?a`]) qed -lemma - assumes "P <-> P" (is "?p <-> _") - shows "?p <-> ?p" - . - text {* Interpretation between locales: sublocales *}