# 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 *}