# HG changeset patch
# User ballarin
# Date 1257972838 -3600
# Node ID bfee47887ca31e01b47e6341ae352b9d807e2314
# Parent  69f0a6271825c69cba97bcaba967dd7494e58d0d
Enables tests for locale functionality that is now available.

diff -r 69f0a6271825 -r bfee47887ca3 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 *}