Enables tests for locale functionality that is now available.
authorballarin
Wed, 11 Nov 2009 21:53:58 +0100
changeset 33617 bfee47887ca3
parent 33616 69f0a6271825
child 33618 d8359a16e0c5
child 33635 dcaada178c6f
child 33835 d6134fb5a49f
Enables tests for locale functionality that is now available.
src/FOL/ex/LocaleTest.thy
--- 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 *}