Enables tests for locale functionality that is now available.
--- a/src/FOL/ex/LocaleTest.thy Wed Nov 11 17:27:48 2009 +0100
+++ b/src/FOL/ex/LocaleTest.thy Wed Nov 11 21:53:58 2009 +0100
@@ -453,8 +453,7 @@
subsection {* Interpretation in theory, then sublocale *}
-interpretation (* fol: *) logic "op +" "minus"
-(* FIXME declaration of qualified names *)
+interpretation fol: logic "op +" "minus"
by unfold_locales (rule int_assoc int_minus2)+
locale logic2 =
@@ -464,17 +463,15 @@
and notnot: "-- (-- x) = x"
begin
-(* FIXME interpretation below fails
definition lor (infixl "||" 50) where
"x || y = --(-- x && -- y)"
-*)
end
sublocale logic < two: logic2
by unfold_locales (rule assoc notnot)+
-thm two.assoc
+thm fol.two.assoc
subsection {* Declarations and sublocale *}