# HG changeset patch
# User ballarin
# Date 1274901618 -7200
# Node ID 29bd6c2ffba859520a2ff12bb6440246c9021f41
# Parent  1d048c6940c867bba8527a69147173c9f03dbc9b
Revise locale test theory layout.

diff -r 1d048c6940c8 -r 29bd6c2ffba8 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Wed May 26 21:20:18 2010 +0200
+++ b/src/FOL/IsaMakefile	Wed May 26 21:20:18 2010 +0200
@@ -46,7 +46,9 @@
 
 $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy		\
   ex/Iff_Oracle.thy ex/Nat.thy ex/Nat_Class.thy ex/Natural_Numbers.thy	\
-  ex/LocaleTest.thy ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML		\
+  ex/Locale_Test/Locale_Test.thy ex/Locale_Test/Locale_Test1.thy	\
+  ex/Locale_Test/Locale_Test2.thy ex/Locale_Test/Locale_Test3.thy	\
+  ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML				\
   ex/Classical.thy ex/document/root.tex ex/Foundation.thy		\
   ex/Intuitionistic.thy ex/Intro.thy ex/Propositional_Int.thy		\
   ex/Propositional_Cla.thy ex/Quantifiers_Int.thy			\
diff -r 1d048c6940c8 -r 29bd6c2ffba8 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Wed May 26 21:20:18 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,712 +0,0 @@
-(*  Title:      FOL/ex/LocaleTest.thy
-    Author:     Clemens Ballarin, TU Muenchen
-
-Test environment for the locale implementation.
-*)
-
-theory LocaleTest
-imports FOL
-begin
-
-typedecl int arities int :: "term"
-consts plus :: "int => int => int" (infixl "+" 60)
-  zero :: int ("0")
-  minus :: "int => int" ("- _")
-
-axioms
-  int_assoc: "(x + y::int) + z = x + (y + z)"
-  int_zero: "0 + x = x"
-  int_minus: "(-x) + x = 0"
-  int_minus2: "-(-x) = x"
-
-section {* Inference of parameter types *}
-
-locale param1 = fixes p
-print_locale! param1
-
-locale param2 = fixes p :: 'b
-print_locale! param2
-
-(*
-locale param_top = param2 r for r :: "'b :: {}"
-  Fails, cannot generalise parameter.
-*)
-
-locale param3 = fixes p (infix ".." 50)
-print_locale! param3
-
-locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
-print_locale! param4
-
-
-subsection {* Incremental type constraints *}
-
-locale constraint1 =
-  fixes  prod (infixl "**" 65)
-  assumes l_id: "x ** y = x"
-  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
-print_locale! constraint1
-
-locale constraint2 =
-  fixes p and q
-  assumes "p = q"
-print_locale! constraint2
-
-
-section {* Inheritance *}
-
-locale semi =
-  fixes prod (infixl "**" 65)
-  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
-print_locale! semi thm semi_def
-
-locale lgrp = semi +
-  fixes one and inv
-  assumes lone: "one ** x = x"
-    and linv: "inv(x) ** x = one"
-print_locale! lgrp thm lgrp_def lgrp_axioms_def
-
-locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +
-  fixes zero and neg
-  assumes lzero: "zero ++ x = x"
-    and lneg: "neg(x) ++ x = zero"
-print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
-
-locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
-print_locale! rev_lgrp thm rev_lgrp_def
-
-locale hom = f: semi f + g: semi g for f and g
-print_locale! hom thm hom_def
-
-locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta
-print_locale! perturbation thm perturbation_def
-
-locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
-print_locale! pert_hom thm pert_hom_def
-
-text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *}
-locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
-print_locale! pert_hom' thm pert_hom'_def
-
-
-section {* Syntax declarations *}
-
-locale logic =
-  fixes land (infixl "&&" 55)
-    and lnot ("-- _" [60] 60)
-  assumes assoc: "(x && y) && z = x && (y && z)"
-    and notnot: "-- (-- x) = x"
-begin
-
-definition lor (infixl "||" 50) where
-  "x || y = --(-- x && -- y)"
-
-end
-print_locale! logic
-
-locale use_decl = logic + semi "op ||"
-print_locale! use_decl thm use_decl_def
-
-locale extra_type =
-  fixes a :: 'a
-    and P :: "'a => 'b => o"
-begin
-
-definition test :: "'a => o" where
-  "test(x) <-> (ALL b. P(x, b))"
-
-end
-
-term extra_type.test thm extra_type.test_def
-
-interpretation var?: extra_type "0" "%x y. x = 0" .
-
-thm var.test_def
-
-
-text {* Under which circumstances term syntax remains active. *}
-
-locale "syntax" =
-  fixes p1 :: "'a => 'b"
-    and p2 :: "'b => o"
-begin
-
-definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))"
-definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)"
-
-thm d1_def d2_def
-
-end
-
-thm syntax.d1_def syntax.d2_def
-
-locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
-begin
-
-thm d1_def d2_def  (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *)
-
-ML {*
-  fun check_syntax ctxt thm expected =
-    let
-      val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
-    in
-      if obtained <> expected
-      then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
-      else ()
-    end;
-*}
-
-ML {*
-  check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
-  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
-*}
-
-end
-
-locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o"
-begin
-
-thm d1_def d2_def
-  (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
-
-ML {*
-  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))";
-  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
-*}
-
-end
-
-
-section {* Foundational versions of theorems *}
-
-thm logic.assoc
-thm logic.lor_def
-
-
-section {* Defines *}
-
-locale logic_def =
-  fixes land (infixl "&&" 55)
-    and lor (infixl "||" 50)
-    and lnot ("-- _" [60] 60)
-  assumes assoc: "(x && y) && z = x && (y && z)"
-    and notnot: "-- (-- x) = x"
-  defines "x || y == --(-- x && -- y)"
-begin
-
-thm lor_def
-
-lemma "x || y = --(-- x && --y)"
-  by (unfold lor_def) (rule refl)
-
-end
-
-(* Inheritance of defines *)
-
-locale logic_def2 = logic_def
-begin
-
-lemma "x || y = --(-- x && --y)"
-  by (unfold lor_def) (rule refl)
-
-end
-
-
-section {* Notes *}
-
-(* A somewhat arcane homomorphism example *)
-
-definition semi_hom where
-  "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
-
-lemma semi_hom_mult:
-  "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
-  by (simp add: semi_hom_def)
-
-locale semi_hom_loc = prod: semi prod + sum: semi sum
-  for prod and sum and h +
-  assumes semi_homh: "semi_hom(prod, sum, h)"
-  notes semi_hom_mult = semi_hom_mult [OF semi_homh]
-
-thm semi_hom_loc.semi_hom_mult
-(* unspecified, attribute not applied in backgroud theory !!! *)
-
-lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
-  by (rule semi_hom_mult)
-
-(* Referring to facts from within a context specification *)
-
-lemma
-  assumes x: "P <-> P"
-  notes y = x
-  shows True ..
-
-
-section {* Theorem statements *}
-
-lemma (in lgrp) lcancel:
-  "x ** y = x ** z <-> y = z"
-proof
-  assume "x ** y = x ** z"
-  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
-  then show "y = z" by (simp add: lone linv)
-qed simp
-print_locale! lgrp
-
-
-locale rgrp = semi +
-  fixes one and inv
-  assumes rone: "x ** one = x"
-    and rinv: "x ** inv(x) = one"
-begin
-
-lemma rcancel:
-  "y ** x = z ** x <-> y = z"
-proof
-  assume "y ** x = z ** x"
-  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
-    by (simp add: assoc [symmetric])
-  then show "y = z" by (simp add: rone rinv)
-qed simp
-
-end
-print_locale! rgrp
-
-
-subsection {* Patterns *}
-
-lemma (in rgrp)
-  assumes "y ** x = z ** x" (is ?a)
-  shows "y = z" (is ?t)
-proof -
-  txt {* Weird proof involving patterns from context element and conclusion. *}
-  {
-    assume ?a
-    then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
-      by (simp add: assoc [symmetric])
-    then have ?t by (simp add: rone rinv)
-  }
-  note x = this
-  show ?t by (rule x [OF `?a`])
-qed
-
-
-section {* Interpretation between locales: sublocales *}
-
-sublocale lgrp < right: rgrp
-print_facts
-proof unfold_locales
-  {
-    fix x
-    have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
-    then show "x ** one = x" by (simp add: assoc lcancel)
-  }
-  note rone = this
-  {
-    fix x
-    have "inv(x) ** x ** inv(x) = inv(x) ** one"
-      by (simp add: linv lone rone)
-    then show "x ** inv(x) = one" by (simp add: assoc lcancel)
-  }
-qed
-
-(* effect on printed locale *)
-
-print_locale! lgrp
-
-(* use of derived theorem *)
-
-lemma (in lgrp)
-  "y ** x = z ** x <-> y = z"
-  apply (rule rcancel)
-  done
-
-(* circular interpretation *)
-
-sublocale rgrp < left: lgrp
-proof unfold_locales
-  {
-    fix x
-    have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
-    then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
-  }
-  note lone = this
-  {
-    fix x
-    have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
-      by (simp add: rinv lone rone)
-    then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
-  }
-qed
-
-(* effect on printed locale *)
-
-print_locale! rgrp
-print_locale! lgrp
-
-
-(* Duality *)
-
-locale order =
-  fixes less :: "'a => 'a => o" (infix "<<" 50)
-  assumes refl: "x << x"
-    and trans: "[| x << y; y << z |] ==> x << z"
-
-sublocale order < dual: order "%x y. y << x"
-  apply unfold_locales apply (rule refl) apply (blast intro: trans)
-  done
-
-print_locale! order  (* Only two instances of order. *)
-
-locale order' =
-  fixes less :: "'a => 'a => o" (infix "<<" 50)
-  assumes refl: "x << x"
-    and trans: "[| x << y; y << z |] ==> x << z"
-
-locale order_with_def = order'
-begin
-
-definition greater :: "'a => 'a => o" (infix ">>" 50) where
-  "x >> y <-> y << x"
-
-end
-
-sublocale order_with_def < dual: order' "op >>"
-  apply unfold_locales
-  unfolding greater_def
-  apply (rule refl) apply (blast intro: trans)
-  done
-
-print_locale! order_with_def
-(* Note that decls come after theorems that make use of them. *)
-
-
-(* locale with many parameters ---
-   interpretations generate alternating group A5 *)
-
-
-locale A5 =
-  fixes A and B and C and D and E
-  assumes eq: "A <-> B <-> C <-> D <-> E"
-
-sublocale A5 < 1: A5 _ _ D E C
-print_facts
-  using eq apply (blast intro: A5.intro) done
-
-sublocale A5 < 2: A5 C _ E _ A
-print_facts
-  using eq apply (blast intro: A5.intro) done
-
-sublocale A5 < 3: A5 B C A _ _
-print_facts
-  using eq apply (blast intro: A5.intro) done
-
-(* Any even permutation of parameters is subsumed by the above. *)
-
-print_locale! A5
-
-
-(* Free arguments of instance *)
-
-locale trivial =
-  fixes P and Q :: o
-  assumes Q: "P <-> P <-> Q"
-begin
-
-lemma Q_triv: "Q" using Q by fast
-
-end
-
-sublocale trivial < x: trivial x _
-  apply unfold_locales using Q by fast
-
-print_locale! trivial
-
-context trivial begin thm x.Q [where ?x = True] end
-
-sublocale trivial < y: trivial Q Q
-  by unfold_locales
-  (* Succeeds since previous interpretation is more general. *)
-
-print_locale! trivial  (* No instance for y created (subsumed). *)
-
-
-subsection {* Sublocale, then interpretation in theory *}
-
-interpretation int?: lgrp "op +" "0" "minus"
-proof unfold_locales
-qed (rule int_assoc int_zero int_minus)+
-
-thm int.assoc int.semi_axioms
-
-interpretation int2?: semi "op +"
-  by unfold_locales  (* subsumed, thm int2.assoc not generated *)
-
-ML {* (PureThy.get_thms @{theory} "int2.assoc";
-    error "thm int2.assoc was generated")
-  handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
-
-thm int.lone int.right.rone
-  (* the latter comes through the sublocale relation *)
-
-
-subsection {* Interpretation in theory, then sublocale *}
-
-interpretation fol: logic "op +" "minus"
-  by unfold_locales (rule int_assoc int_minus2)+
-
-locale logic2 =
-  fixes land (infixl "&&" 55)
-    and lnot ("-- _" [60] 60)
-  assumes assoc: "(x && y) && z = x && (y && z)"
-    and notnot: "-- (-- x) = x"
-begin
-
-definition lor (infixl "||" 50) where
-  "x || y = --(-- x && -- y)"
-
-end
-
-sublocale logic < two: logic2
-  by unfold_locales (rule assoc notnot)+
-
-thm fol.two.assoc
-
-
-subsection {* Declarations and sublocale *}
-
-locale logic_a = logic
-locale logic_b = logic
-
-sublocale logic_a < logic_b
-  by unfold_locales
-
-
-subsection {* Equations *}
-
-locale logic_o =
-  fixes land (infixl "&&" 55)
-    and lnot ("-- _" [60] 60)
-  assumes assoc_o: "(x && y) && z <-> x && (y && z)"
-    and notnot_o: "-- (-- x) <-> x"
-begin
-
-definition lor_o (infixl "||" 50) where
-  "x || y <-> --(-- x && -- y)"
-
-end
-
-interpretation x: logic_o "op &" "Not"
-  where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
-proof -
-  show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
-  show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
-    by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
-qed
-
-thm x.lor_o_def bool_logic_o
-
-lemma lor_triv: "z <-> z" ..
-
-lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
-
-thm lor_triv [where z = True] (* Check strict prefix. *)
-  x.lor_triv
-
-
-subsection {* Inheritance of mixins *}
-
-locale reflexive =
-  fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
-  assumes refl: "x \<sqsubseteq> x"
-begin
-
-definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <-> x \<sqsubseteq> y & x ~= y"
-
-end
-
-consts
-  gle :: "'a => 'a => o" gless :: "'a => 'a => o"
-  gle' :: "'a => 'a => o" gless' :: "'a => 'a => o"
-
-axioms
-  grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
-  grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
-
-text {* Setup *}
-
-locale mixin = reflexive
-begin
-lemmas less_thm = less_def
-end
-
-interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)"
-proof -
-  show "mixin(gle)" by unfold_locales (rule grefl)
-  note reflexive = this[unfolded mixin_def]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
-    by (simp add: reflexive.less_def[OF reflexive] gless_def)
-qed
-
-text {* Mixin propagated along the locale hierarchy *}
-
-locale mixin2 = mixin
-begin
-lemmas less_thm2 = less_def
-end
-
-interpretation le: mixin2 gle
-  by unfold_locales
-
-thm le.less_thm2  (* mixin applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
-  by (rule le.less_thm2)
-
-text {* Mixin does not leak to a side branch. *}
-
-locale mixin3 = reflexive
-begin
-lemmas less_thm3 = less_def
-end
-
-interpretation le: mixin3 gle
-  by unfold_locales
-
-thm le.less_thm3  (* mixin not applied *)
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
-
-text {* Mixin only available in original context *}
-
-locale mixin4_base = reflexive
-
-locale mixin4_mixin = mixin4_base
-
-interpretation le: mixin4_mixin gle
-  where "reflexive.less(gle, x, y) <-> gless(x, y)"
-proof -
-  show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
-  note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
-    by (simp add: reflexive.less_def[OF reflexive] gless_def)
-qed
-
-locale mixin4_copy = mixin4_base
-begin
-lemmas less_thm4 = less_def
-end
-
-locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le
-begin
-lemmas less_thm4' = less_def
-end
-
-interpretation le4: mixin4_combined gle' gle
-  by unfold_locales (rule grefl')
-
-thm le4.less_thm4' (* mixin not applied *)
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
-  by (rule le4.less_thm4')
-
-text {* Inherited mixin applied to new theorem *}
-
-locale mixin5_base = reflexive
-
-locale mixin5_inherited = mixin5_base
-
-interpretation le5: mixin5_base gle
-  where "reflexive.less(gle, x, y) <-> gless(x, y)"
-proof -
-  show "mixin5_base(gle)" by unfold_locales
-  note reflexive = this[unfolded mixin5_base_def mixin_def]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
-    by (simp add: reflexive.less_def[OF reflexive] gless_def)
-qed
-
-interpretation le5: mixin5_inherited gle
-  by unfold_locales
-
-lemmas (in mixin5_inherited) less_thm5 = less_def
-
-thm le5.less_thm5  (* mixin applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
-  by (rule le5.less_thm5)
-
-text {* Mixin pushed down to existing inherited locale *}
-
-locale mixin6_base = reflexive
-
-locale mixin6_inherited = mixin5_base
-
-interpretation le6: mixin6_base gle
-  by unfold_locales
-interpretation le6: mixin6_inherited gle
-  by unfold_locales
-interpretation le6: mixin6_base gle
-  where "reflexive.less(gle, x, y) <-> gless(x, y)"
-proof -
-  show "mixin6_base(gle)" by unfold_locales
-  note reflexive = this[unfolded mixin6_base_def mixin_def]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
-    by (simp add: reflexive.less_def[OF reflexive] gless_def)
-qed
-
-lemmas (in mixin6_inherited) less_thm6 = less_def
-
-thm le6.less_thm6  (* mixin applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
-  by (rule le6.less_thm6)
-
-text {* Existing mixin inherited through sublocale relation *}
-
-locale mixin7_base = reflexive
-
-locale mixin7_inherited = reflexive
-
-interpretation le7: mixin7_base gle
-  where "reflexive.less(gle, x, y) <-> gless(x, y)"
-proof -
-  show "mixin7_base(gle)" by unfold_locales
-  note reflexive = this[unfolded mixin7_base_def mixin_def]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
-    by (simp add: reflexive.less_def[OF reflexive] gless_def)
-qed
-
-interpretation le7: mixin7_inherited gle
-  by unfold_locales
-
-lemmas (in mixin7_inherited) less_thm7 = less_def
-
-thm le7.less_thm7  (* before, mixin not applied *)
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
-  by (rule le7.less_thm7)
-
-sublocale mixin7_inherited < mixin7_base
-  by unfold_locales
-
-lemmas (in mixin7_inherited) less_thm7b = less_def
-
-thm le7.less_thm7b  (* after, mixin applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
-  by (rule le7.less_thm7b)
-
-
-subsection {* Interpretation in proofs *}
-
-lemma True
-proof
-  interpret "local": lgrp "op +" "0" "minus"
-    by unfold_locales  (* subsumed *)
-  {
-    fix zero :: int
-    assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
-    then interpret local_fixed: lgrp "op +" zero "minus"
-      by unfold_locales
-    thm local_fixed.lone
-  }
-  assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
-  then interpret local_free: lgrp "op +" zero "minus" for zero
-    by unfold_locales
-  thm local_free.lone [where ?zero = 0]
-qed
-
-end
diff -r 1d048c6940c8 -r 29bd6c2ffba8 src/FOL/ex/Locale_Test/Locale_Test.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/Locale_Test/Locale_Test.thy	Wed May 26 21:20:18 2010 +0200
@@ -0,0 +1,24 @@
+(*  Title:      FOL/ex/Locale_Test/Locale_Test.thy
+    Author:     Clemens Ballarin
+
+Test environment for the locale implementation.
+*)
+
+theory Locale_Test
+imports Locale_Test1 Locale_Test2 Locale_Test3
+begin
+
+text {* Result of theory merge with distinct but identical interpretations *}
+
+context mixin_thy_merge
+begin
+lemmas less_mixin_thy_merge1 = le.less_def
+lemmas less_mixin_thy_merge2 = le'.less_def
+end
+
+lemma "gless(x, y) <-> gle(x, y) & x ~= y" (* mixin from first interpretation applied *)
+  by (rule le1.less_mixin_thy_merge1)
+lemma "gless'(x, y) <-> gle'(x, y) & x ~= y" (* mixin from second interpretation applied *)
+  by (rule le1.less_mixin_thy_merge2)
+
+end
diff -r 1d048c6940c8 -r 29bd6c2ffba8 src/FOL/ex/Locale_Test/Locale_Test1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Wed May 26 21:20:18 2010 +0200
@@ -0,0 +1,717 @@
+(*  Title:      FOL/ex/Locale_Test/Locale_Test1.thy
+    Author:     Clemens Ballarin, TU Muenchen
+
+Test environment for the locale implementation.
+*)
+
+theory Locale_Test1
+imports FOL
+begin
+
+typedecl int arities int :: "term"
+consts plus :: "int => int => int" (infixl "+" 60)
+  zero :: int ("0")
+  minus :: "int => int" ("- _")
+
+axioms
+  int_assoc: "(x + y::int) + z = x + (y + z)"
+  int_zero: "0 + x = x"
+  int_minus: "(-x) + x = 0"
+  int_minus2: "-(-x) = x"
+
+section {* Inference of parameter types *}
+
+locale param1 = fixes p
+print_locale! param1
+
+locale param2 = fixes p :: 'b
+print_locale! param2
+
+(*
+locale param_top = param2 r for r :: "'b :: {}"
+  Fails, cannot generalise parameter.
+*)
+
+locale param3 = fixes p (infix ".." 50)
+print_locale! param3
+
+locale param4 = fixes p :: "'a => 'a => 'a" (infix ".." 50)
+print_locale! param4
+
+
+subsection {* Incremental type constraints *}
+
+locale constraint1 =
+  fixes  prod (infixl "**" 65)
+  assumes l_id: "x ** y = x"
+  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+print_locale! constraint1
+
+locale constraint2 =
+  fixes p and q
+  assumes "p = q"
+print_locale! constraint2
+
+
+section {* Inheritance *}
+
+locale semi =
+  fixes prod (infixl "**" 65)
+  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
+print_locale! semi thm semi_def
+
+locale lgrp = semi +
+  fixes one and inv
+  assumes lone: "one ** x = x"
+    and linv: "inv(x) ** x = one"
+print_locale! lgrp thm lgrp_def lgrp_axioms_def
+
+locale add_lgrp = semi "op ++" for sum (infixl "++" 60) +
+  fixes zero and neg
+  assumes lzero: "zero ++ x = x"
+    and lneg: "neg(x) ++ x = zero"
+print_locale! add_lgrp thm add_lgrp_def add_lgrp_axioms_def
+
+locale rev_lgrp = semi "%x y. y ++ x" for sum (infixl "++" 60)
+print_locale! rev_lgrp thm rev_lgrp_def
+
+locale hom = f: semi f + g: semi g for f and g
+print_locale! hom thm hom_def
+
+locale perturbation = semi + d: semi "%x y. delta(x) ** delta(y)" for delta
+print_locale! perturbation thm perturbation_def
+
+locale pert_hom = d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
+print_locale! pert_hom thm pert_hom_def
+
+text {* Alternative expression, obtaining nicer names in @{text "semi f"}. *}
+locale pert_hom' = semi f + d1: perturbation f d1 + d2: perturbation f d2 for f d1 d2
+print_locale! pert_hom' thm pert_hom'_def
+
+
+section {* Syntax declarations *}
+
+locale logic =
+  fixes land (infixl "&&" 55)
+    and lnot ("-- _" [60] 60)
+  assumes assoc: "(x && y) && z = x && (y && z)"
+    and notnot: "-- (-- x) = x"
+begin
+
+definition lor (infixl "||" 50) where
+  "x || y = --(-- x && -- y)"
+
+end
+print_locale! logic
+
+locale use_decl = logic + semi "op ||"
+print_locale! use_decl thm use_decl_def
+
+locale extra_type =
+  fixes a :: 'a
+    and P :: "'a => 'b => o"
+begin
+
+definition test :: "'a => o" where
+  "test(x) <-> (ALL b. P(x, b))"
+
+end
+
+term extra_type.test thm extra_type.test_def
+
+interpretation var?: extra_type "0" "%x y. x = 0" .
+
+thm var.test_def
+
+
+text {* Under which circumstances term syntax remains active. *}
+
+locale "syntax" =
+  fixes p1 :: "'a => 'b"
+    and p2 :: "'b => o"
+begin
+
+definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))"
+definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)"
+
+thm d1_def d2_def
+
+end
+
+thm syntax.d1_def syntax.d2_def
+
+locale syntax' = "syntax" p1 p2 for p1 :: "'a => 'a" and p2 :: "'a => o"
+begin
+
+thm d1_def d2_def  (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *)
+
+ML {*
+  fun check_syntax ctxt thm expected =
+    let
+      val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
+    in
+      if obtained <> expected
+      then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
+      else ()
+    end;
+*}
+
+ML {*
+  check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
+  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
+*}
+
+end
+
+locale syntax'' = "syntax" p3 p2 for p3 :: "'a => 'b" and p2 :: "'b => o"
+begin
+
+thm d1_def d2_def
+  (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
+
+ML {*
+  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))";
+  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
+*}
+
+end
+
+
+section {* Foundational versions of theorems *}
+
+thm logic.assoc
+thm logic.lor_def
+
+
+section {* Defines *}
+
+locale logic_def =
+  fixes land (infixl "&&" 55)
+    and lor (infixl "||" 50)
+    and lnot ("-- _" [60] 60)
+  assumes assoc: "(x && y) && z = x && (y && z)"
+    and notnot: "-- (-- x) = x"
+  defines "x || y == --(-- x && -- y)"
+begin
+
+thm lor_def
+
+lemma "x || y = --(-- x && --y)"
+  by (unfold lor_def) (rule refl)
+
+end
+
+(* Inheritance of defines *)
+
+locale logic_def2 = logic_def
+begin
+
+lemma "x || y = --(-- x && --y)"
+  by (unfold lor_def) (rule refl)
+
+end
+
+
+section {* Notes *}
+
+(* A somewhat arcane homomorphism example *)
+
+definition semi_hom where
+  "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
+
+lemma semi_hom_mult:
+  "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
+  by (simp add: semi_hom_def)
+
+locale semi_hom_loc = prod: semi prod + sum: semi sum
+  for prod and sum and h +
+  assumes semi_homh: "semi_hom(prod, sum, h)"
+  notes semi_hom_mult = semi_hom_mult [OF semi_homh]
+
+thm semi_hom_loc.semi_hom_mult
+(* unspecified, attribute not applied in backgroud theory !!! *)
+
+lemma (in semi_hom_loc) "h(prod(x, y)) = sum(h(x), h(y))"
+  by (rule semi_hom_mult)
+
+(* Referring to facts from within a context specification *)
+
+lemma
+  assumes x: "P <-> P"
+  notes y = x
+  shows True ..
+
+
+section {* Theorem statements *}
+
+lemma (in lgrp) lcancel:
+  "x ** y = x ** z <-> y = z"
+proof
+  assume "x ** y = x ** z"
+  then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
+  then show "y = z" by (simp add: lone linv)
+qed simp
+print_locale! lgrp
+
+
+locale rgrp = semi +
+  fixes one and inv
+  assumes rone: "x ** one = x"
+    and rinv: "x ** inv(x) = one"
+begin
+
+lemma rcancel:
+  "y ** x = z ** x <-> y = z"
+proof
+  assume "y ** x = z ** x"
+  then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
+    by (simp add: assoc [symmetric])
+  then show "y = z" by (simp add: rone rinv)
+qed simp
+
+end
+print_locale! rgrp
+
+
+subsection {* Patterns *}
+
+lemma (in rgrp)
+  assumes "y ** x = z ** x" (is ?a)
+  shows "y = z" (is ?t)
+proof -
+  txt {* Weird proof involving patterns from context element and conclusion. *}
+  {
+    assume ?a
+    then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
+      by (simp add: assoc [symmetric])
+    then have ?t by (simp add: rone rinv)
+  }
+  note x = this
+  show ?t by (rule x [OF `?a`])
+qed
+
+
+section {* Interpretation between locales: sublocales *}
+
+sublocale lgrp < right: rgrp
+print_facts
+proof unfold_locales
+  {
+    fix x
+    have "inv(x) ** x ** one = inv(x) ** x" by (simp add: linv lone)
+    then show "x ** one = x" by (simp add: assoc lcancel)
+  }
+  note rone = this
+  {
+    fix x
+    have "inv(x) ** x ** inv(x) = inv(x) ** one"
+      by (simp add: linv lone rone)
+    then show "x ** inv(x) = one" by (simp add: assoc lcancel)
+  }
+qed
+
+(* effect on printed locale *)
+
+print_locale! lgrp
+
+(* use of derived theorem *)
+
+lemma (in lgrp)
+  "y ** x = z ** x <-> y = z"
+  apply (rule rcancel)
+  done
+
+(* circular interpretation *)
+
+sublocale rgrp < left: lgrp
+proof unfold_locales
+  {
+    fix x
+    have "one ** (x ** inv(x)) = x ** inv(x)" by (simp add: rinv rone)
+    then show "one ** x = x" by (simp add: assoc [symmetric] rcancel)
+  }
+  note lone = this
+  {
+    fix x
+    have "inv(x) ** (x ** inv(x)) = one ** inv(x)"
+      by (simp add: rinv lone rone)
+    then show "inv(x) ** x = one" by (simp add: assoc [symmetric] rcancel)
+  }
+qed
+
+(* effect on printed locale *)
+
+print_locale! rgrp
+print_locale! lgrp
+
+
+(* Duality *)
+
+locale order =
+  fixes less :: "'a => 'a => o" (infix "<<" 50)
+  assumes refl: "x << x"
+    and trans: "[| x << y; y << z |] ==> x << z"
+
+sublocale order < dual: order "%x y. y << x"
+  apply unfold_locales apply (rule refl) apply (blast intro: trans)
+  done
+
+print_locale! order  (* Only two instances of order. *)
+
+locale order' =
+  fixes less :: "'a => 'a => o" (infix "<<" 50)
+  assumes refl: "x << x"
+    and trans: "[| x << y; y << z |] ==> x << z"
+
+locale order_with_def = order'
+begin
+
+definition greater :: "'a => 'a => o" (infix ">>" 50) where
+  "x >> y <-> y << x"
+
+end
+
+sublocale order_with_def < dual: order' "op >>"
+  apply unfold_locales
+  unfolding greater_def
+  apply (rule refl) apply (blast intro: trans)
+  done
+
+print_locale! order_with_def
+(* Note that decls come after theorems that make use of them. *)
+
+
+(* locale with many parameters ---
+   interpretations generate alternating group A5 *)
+
+
+locale A5 =
+  fixes A and B and C and D and E
+  assumes eq: "A <-> B <-> C <-> D <-> E"
+
+sublocale A5 < 1: A5 _ _ D E C
+print_facts
+  using eq apply (blast intro: A5.intro) done
+
+sublocale A5 < 2: A5 C _ E _ A
+print_facts
+  using eq apply (blast intro: A5.intro) done
+
+sublocale A5 < 3: A5 B C A _ _
+print_facts
+  using eq apply (blast intro: A5.intro) done
+
+(* Any even permutation of parameters is subsumed by the above. *)
+
+print_locale! A5
+
+
+(* Free arguments of instance *)
+
+locale trivial =
+  fixes P and Q :: o
+  assumes Q: "P <-> P <-> Q"
+begin
+
+lemma Q_triv: "Q" using Q by fast
+
+end
+
+sublocale trivial < x: trivial x _
+  apply unfold_locales using Q by fast
+
+print_locale! trivial
+
+context trivial begin thm x.Q [where ?x = True] end
+
+sublocale trivial < y: trivial Q Q
+  by unfold_locales
+  (* Succeeds since previous interpretation is more general. *)
+
+print_locale! trivial  (* No instance for y created (subsumed). *)
+
+
+subsection {* Sublocale, then interpretation in theory *}
+
+interpretation int?: lgrp "op +" "0" "minus"
+proof unfold_locales
+qed (rule int_assoc int_zero int_minus)+
+
+thm int.assoc int.semi_axioms
+
+interpretation int2?: semi "op +"
+  by unfold_locales  (* subsumed, thm int2.assoc not generated *)
+
+ML {* (PureThy.get_thms @{theory} "int2.assoc";
+    error "thm int2.assoc was generated")
+  handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
+
+thm int.lone int.right.rone
+  (* the latter comes through the sublocale relation *)
+
+
+subsection {* Interpretation in theory, then sublocale *}
+
+interpretation fol: logic "op +" "minus"
+  by unfold_locales (rule int_assoc int_minus2)+
+
+locale logic2 =
+  fixes land (infixl "&&" 55)
+    and lnot ("-- _" [60] 60)
+  assumes assoc: "(x && y) && z = x && (y && z)"
+    and notnot: "-- (-- x) = x"
+begin
+
+definition lor (infixl "||" 50) where
+  "x || y = --(-- x && -- y)"
+
+end
+
+sublocale logic < two: logic2
+  by unfold_locales (rule assoc notnot)+
+
+thm fol.two.assoc
+
+
+subsection {* Declarations and sublocale *}
+
+locale logic_a = logic
+locale logic_b = logic
+
+sublocale logic_a < logic_b
+  by unfold_locales
+
+
+subsection {* Equations *}
+
+locale logic_o =
+  fixes land (infixl "&&" 55)
+    and lnot ("-- _" [60] 60)
+  assumes assoc_o: "(x && y) && z <-> x && (y && z)"
+    and notnot_o: "-- (-- x) <-> x"
+begin
+
+definition lor_o (infixl "||" 50) where
+  "x || y <-> --(-- x && -- y)"
+
+end
+
+interpretation x: logic_o "op &" "Not"
+  where bool_logic_o: "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+proof -
+  show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
+  show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+    by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
+qed
+
+thm x.lor_o_def bool_logic_o
+
+lemma lor_triv: "z <-> z" ..
+
+lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
+
+thm lor_triv [where z = True] (* Check strict prefix. *)
+  x.lor_triv
+
+
+subsection {* Inheritance of mixins *}
+
+locale reflexive =
+  fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
+  assumes refl: "x \<sqsubseteq> x"
+begin
+
+definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <-> x \<sqsubseteq> y & x ~= y"
+
+end
+
+consts
+  gle :: "'a => 'a => o" gless :: "'a => 'a => o"
+  gle' :: "'a => 'a => o" gless' :: "'a => 'a => o"
+
+axioms
+  grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
+  grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
+
+text {* Setup *}
+
+locale mixin = reflexive
+begin
+lemmas less_thm = less_def
+end
+
+interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+  show "mixin(gle)" by unfold_locales (rule grefl)
+  note reflexive = this[unfolded mixin_def]
+  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+    by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+text {* Mixin propagated along the locale hierarchy *}
+
+locale mixin2 = mixin
+begin
+lemmas less_thm2 = less_def
+end
+
+interpretation le: mixin2 gle
+  by unfold_locales
+
+thm le.less_thm2  (* mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+  by (rule le.less_thm2)
+
+text {* Mixin does not leak to a side branch. *}
+
+locale mixin3 = reflexive
+begin
+lemmas less_thm3 = less_def
+end
+
+interpretation le: mixin3 gle
+  by unfold_locales
+
+thm le.less_thm3  (* mixin not applied *)
+lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
+
+text {* Mixin only available in original context *}
+
+locale mixin4_base = reflexive
+
+locale mixin4_mixin = mixin4_base
+
+interpretation le: mixin4_mixin gle
+  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+  show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
+  note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
+  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+    by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+locale mixin4_copy = mixin4_base
+begin
+lemmas less_thm4 = less_def
+end
+
+locale mixin4_combined = le1: mixin4_mixin le' + le2: mixin4_copy le for le' le
+begin
+lemmas less_thm4' = less_def
+end
+
+interpretation le4: mixin4_combined gle' gle
+  by unfold_locales (rule grefl')
+
+thm le4.less_thm4' (* mixin not applied *)
+lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+  by (rule le4.less_thm4')
+
+text {* Inherited mixin applied to new theorem *}
+
+locale mixin5_base = reflexive
+
+locale mixin5_inherited = mixin5_base
+
+interpretation le5: mixin5_base gle
+  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+  show "mixin5_base(gle)" by unfold_locales
+  note reflexive = this[unfolded mixin5_base_def mixin_def]
+  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+    by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+interpretation le5: mixin5_inherited gle
+  by unfold_locales
+
+lemmas (in mixin5_inherited) less_thm5 = less_def
+
+thm le5.less_thm5  (* mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+  by (rule le5.less_thm5)
+
+text {* Mixin pushed down to existing inherited locale *}
+
+locale mixin6_base = reflexive
+
+locale mixin6_inherited = mixin5_base
+
+interpretation le6: mixin6_base gle
+  by unfold_locales
+interpretation le6: mixin6_inherited gle
+  by unfold_locales
+interpretation le6: mixin6_base gle
+  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+  show "mixin6_base(gle)" by unfold_locales
+  note reflexive = this[unfolded mixin6_base_def mixin_def]
+  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+    by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+lemmas (in mixin6_inherited) less_thm6 = less_def
+
+thm le6.less_thm6  (* mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+  by (rule le6.less_thm6)
+
+text {* Existing mixin inherited through sublocale relation *}
+
+locale mixin7_base = reflexive
+
+locale mixin7_inherited = reflexive
+
+interpretation le7: mixin7_base gle
+  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+  show "mixin7_base(gle)" by unfold_locales
+  note reflexive = this[unfolded mixin7_base_def mixin_def]
+  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+    by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+interpretation le7: mixin7_inherited gle
+  by unfold_locales
+
+lemmas (in mixin7_inherited) less_thm7 = less_def
+
+thm le7.less_thm7  (* before, mixin not applied *)
+lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+  by (rule le7.less_thm7)
+
+sublocale mixin7_inherited < mixin7_base
+  by unfold_locales
+
+lemmas (in mixin7_inherited) less_thm7b = less_def
+
+thm le7.less_thm7b  (* after, mixin applied *)
+lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+  by (rule le7.less_thm7b)
+
+
+text {* This locale will be interpreted in later theories. *}
+
+locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le'
+
+
+subsection {* Interpretation in proofs *}
+
+lemma True
+proof
+  interpret "local": lgrp "op +" "0" "minus"
+    by unfold_locales  (* subsumed *)
+  {
+    fix zero :: int
+    assume "!!x. zero + x = x" "!!x. (-x) + x = zero"
+    then interpret local_fixed: lgrp "op +" zero "minus"
+      by unfold_locales
+    thm local_fixed.lone
+  }
+  assume "!!x zero. zero + x = x" "!!x zero. (-x) + x = zero"
+  then interpret local_free: lgrp "op +" zero "minus" for zero
+    by unfold_locales
+  thm local_free.lone [where ?zero = 0]
+qed
+
+end
diff -r 1d048c6940c8 -r 29bd6c2ffba8 src/FOL/ex/Locale_Test/Locale_Test2.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/Locale_Test/Locale_Test2.thy	Wed May 26 21:20:18 2010 +0200
@@ -0,0 +1,20 @@
+(*  Title:      FOL/ex/Locale_Test/Locale_Test2.thy
+    Author:     Clemens Ballarin, TU Muenchen
+
+Test environment for the locale implementation.
+*)
+
+theory Locale_Test2
+imports Locale_Test1
+begin
+
+interpretation le1: mixin_thy_merge gle gle'
+  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+proof -
+  show "mixin_thy_merge(gle, gle')" by unfold_locales
+  note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct1]
+  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+    by (simp add: reflexive.less_def[OF reflexive] gless_def)
+qed
+
+end
diff -r 1d048c6940c8 -r 29bd6c2ffba8 src/FOL/ex/Locale_Test/Locale_Test3.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/Locale_Test/Locale_Test3.thy	Wed May 26 21:20:18 2010 +0200
@@ -0,0 +1,20 @@
+(*  Title:      FOL/ex/Locale_Test/Locale_Test3.thy
+    Author:     Clemens Ballarin
+
+Test environment for the locale implementation.
+*)
+
+theory Locale_Test3
+imports Locale_Test1
+begin
+
+interpretation le2: mixin_thy_merge gle gle'
+  where "reflexive.less(gle', x, y) <-> gless'(x, y)"
+proof -
+  show "mixin_thy_merge(gle, gle')" by unfold_locales
+  note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct2]
+  show "reflexive.less(gle', x, y) <-> gless'(x, y)"
+    by (simp add: reflexive.less_def[OF reflexive] gless'_def)
+qed
+
+end
diff -r 1d048c6940c8 -r 29bd6c2ffba8 src/FOL/ex/ROOT.ML
--- a/src/FOL/ex/ROOT.ML	Wed May 26 21:20:18 2010 +0200
+++ b/src/FOL/ex/ROOT.ML	Wed May 26 21:20:18 2010 +0200
@@ -23,4 +23,4 @@
 ];
 
 (*regression test for locales -- sets several global flags!*)
-no_document use_thy "LocaleTest";
+no_document use_thy "Locale_Test/Locale_Test";