All logics ported to new locales.

--- a/src/FOL/IsaMakefile	Fri Dec 19 15:05:37 2008 +0100
+++ b/src/FOL/IsaMakefile	Fri Dec 19 16:39:23 2008 +0100
@@ -46,7 +46,7 @@
 FOL-ex: FOL $(LOG)/FOL-ex.gz
 
 $(LOG)/FOL-ex.gz: $(OUT)/FOL ex/First_Order_Logic.thy ex/If.thy		\
-  ex/IffOracle.thy ex/LocaleTest.thy ex/Nat.thy ex/Natural_Numbers.thy	\
+  ex/IffOracle.thy ex/Nat.thy ex/Natural_Numbers.thy	\
   ex/NewLocaleSetup.thy ex/NewLocaleTest.thy    \
   ex/Miniscope.thy ex/Prolog.thy ex/ROOT.ML ex/Classical.thy		\
   ex/document/root.tex ex/Foundation.thy ex/Intuitionistic.thy		\

--- a/src/FOL/ex/LocaleTest.thy	Fri Dec 19 15:05:37 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,765 +0,0 @@
-(*  Title:      FOL/ex/LocaleTest.thy
-    ID:         $Id$
-    Author:     Clemens Ballarin
-    Copyright (c) 2005 by Clemens Ballarin
-
-Collection of regression tests for locales.
-*)
-
-header {* Test of Locale Interpretation *}
-
-theory LocaleTest
-imports FOL
-begin
-
-ML {* set Toplevel.debug *}
-ML {* set show_hyps *}
-ML {* set show_sorts *}
-
-ML {*
-  fun check_thm name = let
-    val thy = the_context ();
-    val thm = PureThy.get_thm thy name;
-    val {prop, hyps, ...} = rep_thm thm;
-    val prems = Logic.strip_imp_prems prop;
-    val _ = if null hyps then ()
-        else error ("Theorem " ^ quote name ^ " has meta hyps.\n" ^
-          "Consistency check of locales package failed.");
-    val _ = if null prems then ()
-        else error ("Theorem " ^ quote name ^ " has premises.\n" ^
-          "Consistency check of locales package failed.");
-  in () end;
-*}
-
-section {* Context Elements and Locale Expressions *}
-
-text {* Naming convention for global objects: prefixes L and l *}
-
-subsection {* Renaming with Syntax *}
-
-locale LS = var mult +
-  assumes "mult(x, y) = mult(y, x)"
-
-print_locale LS
-
-locale LS' = LS mult (infixl "**" 60)
-
-print_locale LS'
-
-locale LT = var mult (infixl "**" 60) +
-  assumes "x ** y = y ** x"
-
-locale LU = LT mult (infixl "**" 60) + LT add (infixl "++" 55) + var h +
-  assumes hom: "h(x ** y) = h(x) ++ h(y)"
-
-
-(* FIXME: graceful handling of type errors?
-locale LY = LT mult (infixl "**" 60) + LT add (binder "++" 55) + var h +
-  assumes "mult(x) == add"
-*)
-
-
-locale LV = LU _ add
-
-locale LW = LU _ mult (infixl "**" 60)
-
-
-subsection {* Constrains *}
-
-locale LZ = fixes a (structure)
-locale LZ' = LZ +
-  constrains a :: "'a => 'b"
-  assumes "a (x :: 'a) = a (y)"
-print_locale LZ'
-
-
-section {* Interpretation *}
-
-text {* Naming convention for global objects: prefixes I and i *}
-
-text {* interpretation input syntax *}
-
-locale IL
-locale IM = fixes a and b and c
-
-interpretation test: IL + IM a b c [x y z] .
-
-print_interps IL    (* output: test *)
-print_interps IM    (* output: test *)
-
-interpretation test: IL print_interps IM .
-
-interpretation IL .
-
-text {* Processing of locale expression *}
-
-locale IA = fixes a assumes asm_A: "a = a"
-
-locale IB = fixes b assumes asm_B [simp]: "b = b"
-
-locale IC = IA + IB + assumes asm_C: "b = b"
-
-locale IC' = IA + IB + assumes asm_C: "c = c"
-  (* independent type var in c *)
-
-locale ID = IA + IB + fixes d defines def_D: "d == (a = b)"
-
-theorem (in ID) True ..
-
-typedecl i
-arities i :: "term"
-
-
-interpretation i1: IC ["X::i" "Y::i"] by unfold_locales auto
-
-print_interps IA  (* output: i1 *)
-
-(* possible accesses *)
-thm i1.a.asm_A thm LocaleTest.IA_locale.i1.a.asm_A thm IA_locale.i1.a.asm_A
-thm i1.asm_A thm LocaleTest.i1.asm_A
-
-ML {* check_thm "i1.a.asm_A" *}
-
-(* without prefix *)
-
-interpretation IC ["W::i" "Z::i"] by intro_locales  (* subsumed by i1: IC *)
-interpretation IC ["W::'a" "Z::i"] by unfold_locales auto
-  (* subsumes i1: IA and i1: IC *)
-
-print_interps IA  (* output: <no prefix>, i1 *)
-
-(* possible accesses *)
-thm asm_C thm a_b.asm_C thm LocaleTest.IC_locale.a_b.asm_C thm IC_locale.a_b.asm_C
-
-ML {* check_thm "asm_C" *}
-
-interpretation i2: ID [X "Y::i" "Y = X"]
-  by (simp add: eq_commute) unfold_locales
-
-print_interps IA  (* output: <no prefix>, i1 *)
-print_interps ID  (* output: i2 *)
-
-
-interpretation i3: ID [X "Y::i"] by simp unfold_locales
-
-(* duplicate: thm not added *)
-
-(* thm i3.a.asm_A *)
-
-
-print_interps IA  (* output: <no prefix>, i1 *)
-print_interps IB  (* output: i1 *)
-print_interps IC  (* output: <no prefix, i1 *)
-print_interps ID  (* output: i2, i3 *)
-
-
-interpretation i10: ID + ID a' b' d' [X "Y::i" _ u "v::i" _] by intro_locales
-
-corollary (in ID) th_x: True ..
-
-(* possible accesses: for each registration *)
-
-thm i2.th_x thm i3.th_x
-
-ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
-
-lemma (in ID) th_y: "d == (a = b)" by (rule d_def)
-
-thm i2.th_y thm i3.th_y
-
-ML {* check_thm "i2.th_y"; check_thm "i3.th_y" *}
-
-lemmas (in ID) th_z = th_y
-
-thm i2.th_z
-
-ML {* check_thm "i2.th_z" *}
-
-
-subsection {* Interpretation in Proof Contexts *}
-
-locale IF = fixes f assumes asm_F: "f & f --> f"
-
-consts default :: "'a"
-
-theorem True
-proof -
-  fix alpha::i and beta
-  have alpha_A: "IA(alpha)" by unfold_locales
-  interpret i5: IA [alpha] by intro_locales  (* subsumed *)
-  print_interps IA  (* output: <no prefix>, i1 *)
-  interpret i6: IC [alpha beta] by unfold_locales auto
-  print_interps IA   (* output: <no prefix>, i1 *)
-  print_interps IC   (* output: <no prefix>, i1, i6 *)
-  interpret i11: IF ["default = default"] by (fast intro: IF.intro)
-  thm i11.asm_F [where 'a = i]     (* default has schematic type *)
-qed rule
-
-theorem (in IA) True
-proof -
-  print_interps! IA
-  fix beta and gamma
-  interpret i9: ID [a beta _]
-    apply - apply assumption
-    apply unfold_locales
-    apply (rule refl) done
-qed rule
-
-
-(* Definition involving free variable *)
-
-ML {* reset show_sorts *}
-
-locale IE = fixes e defines e_def: "e(x) == x & x"
-  notes e_def2 = e_def
-
-lemma (in IE) True thm e_def by fast
-
-interpretation i7: IE ["%x. x"] by simp
-
-thm i7.e_def2 (* has no premise *)
-
-ML {* check_thm "i7.e_def2" *}
-
-locale IE' = fixes e defines e_def: "e == (%x. x & x)"
-  notes e_def2 = e_def
-
-interpretation i7': IE' ["(%x. x)"] by simp
-
-thm i7'.e_def2
-
-ML {* check_thm "i7'.e_def2" *}
-
-(* Definition involving free variable in assm *)
-
-locale IG = fixes g assumes asm_G: "g --> x"
-  notes asm_G2 = asm_G
-
-interpretation i8: IG ["False"] by unfold_locales fast
-
-thm i8.asm_G2
-
-ML {* check_thm "i8.asm_G2" *}
-
-text {* Locale without assumptions *}
-
-locale IL1 = notes rev_conjI [intro] = conjI [THEN iffD1 [OF conj_commute]]
-
-lemma "[| P; Q |] ==> P & Q"
-proof -
-  interpret my: IL1 .          txt {* No chained fact required. *}
-  assume Q and P               txt {* order reversed *}
-  then show "P & Q" ..         txt {* Applies @{thm my.rev_conjI}. *}
-qed
-
-locale IL11 = notes rev_conjI = conjI [THEN iffD1 [OF conj_commute]]
-
-
-subsection {* Simple locale with assumptions *}
-
-consts ibin :: "[i, i] => i" (infixl "#" 60)
-
-axioms i_assoc: "(x # y) # z = x # (y # z)"
-  i_comm: "x # y = y # x"
-
-locale IL2 =
-  fixes OP (infixl "+" 60)
-  assumes assoc: "(x + y) + z = x + (y + z)"
-    and comm: "x + y = y + x"
-
-lemma (in IL2) lcomm: "x + (y + z) = y + (x + z)"
-proof -
-  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
-  also have "... = (y + x) + z" by (simp add: comm)
-  also have "... = y + (x + z)" by (simp add: assoc)
-  finally show ?thesis .
-qed
-
-lemmas (in IL2) AC = comm assoc lcomm
-
-lemma "(x::i) # y # z # w = y # x # w # z"
-proof -
-  interpret my: IL2 ["op #"] by (rule IL2.intro [of "op #", OF i_assoc i_comm])
-  show ?thesis by (simp only: my.OP.AC)  (* or my.AC *)
-qed
-
-subsection {* Nested locale with assumptions *}
-
-locale IL3 =
-  fixes OP (infixl "+" 60)
-  assumes assoc: "(x + y) + z = x + (y + z)"
-
-locale IL4 = IL3 +
-  assumes comm: "x + y = y + x"
-
-lemma (in IL4) lcomm: "x + (y + z) = y + (x + z)"
-proof -
-  have "x + (y + z) = (x + y) + z" by (simp add: assoc)
-  also have "... = (y + x) + z" by (simp add: comm)
-  also have "... = y + (x + z)" by (simp add: assoc)
-  finally show ?thesis .
-qed
-
-lemmas (in IL4) AC = comm assoc lcomm
-
-lemma "(x::i) # y # z # w = y # x # w # z"
-proof -
-  interpret my: IL4 ["op #"]
-    by (auto intro: IL4.intro IL3.intro IL4_axioms.intro i_assoc i_comm)
-  show ?thesis by (simp only: my.OP.AC)  (* or simply AC *)
-qed
-
-text {* Locale with definition *}
-
-text {* This example is admittedly not very creative :-) *}
-
-locale IL5 = IL4 + var A +
-  defines A_def: "A == True"
-
-lemma (in IL5) lem: A
-  by (unfold A_def) rule
-
-lemma "IL5(op #) ==> True"
-proof -
-  assume "IL5(op #)"
-  then interpret IL5 ["op #"] by (auto intro: IL5.axioms)
-  show ?thesis by (rule lem)  (* lem instantiated to True *)
-qed
-
-text {* Interpretation in a context with target *}
-
-lemma (in IL4)
-  fixes A (infixl "$" 60)
-  assumes A: "IL4(A)"
-  shows "(x::i) $ y $ z $ w = y $ x $ w $ z"
-proof -
-  from A interpret A: IL4 ["A"] by (auto intro: IL4.axioms)
-  show ?thesis by (simp only: A.OP.AC)
-qed
-
-
-section {* Interpretation in Locales *}
-
-text {* Naming convention for global objects: prefixes R and r *}
-
-(* locale with many parameters ---
-   interpretations generate alternating group A5 *)
-
-locale RA5 = var A + var B + var C + var D + var E +
-  assumes eq: "A <-> B <-> C <-> D <-> E"
-
-interpretation RA5 < RA5 _ _ D E C
-print_facts
-print_interps RA5
-  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
-
-interpretation RA5 < RA5 C _ E _ A
-print_facts
-print_interps RA5
-  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
-
-interpretation RA5 < RA5 B C A _ _
-print_facts
-print_interps RA5
-  using A_B_C_D_E.eq apply (blast intro: RA5.intro) done
-
-interpretation RA5 < RA5 _ C D B _ .
-  (* Any even permutation of parameters is subsumed by the above. *)
-
-(* circle of three locales, forward direction *)
-
-locale RA1 = var A + var B + assumes p: "A <-> B"
-locale RA2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
-locale RA3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
-
-interpretation RA1 < RA2
-  print_facts
-  using p apply unfold_locales apply fast done
-interpretation RA2 < RA3
-  print_facts
-  using q apply unfold_locales apply fast done
-interpretation RA3 < RA1
-  print_facts
-  using r apply unfold_locales apply fast done
-
-(* circle of three locales, backward direction *)
-
-locale RB1 = var A + var B + assumes p: "A <-> B"
-locale RB2 = var A + var B + assumes q: "A & B | ~ A & ~ B"
-locale RB3 = var A + var B + assumes r: "(A --> B) & (B --> A)"
-
-interpretation RB1 < RB2
-  print_facts
-  using p apply unfold_locales apply fast done
-interpretation RB3 < RB1
-  print_facts
-  using r apply unfold_locales apply fast done
-interpretation RB2 < RB3
-  print_facts
-  using q apply unfold_locales apply fast done
-
-lemma (in RB1) True
-  print_facts
-  ..
-
-
-(* Group example *)
-
-locale Rsemi = var prod (infixl "**" 65) +
-  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
-
-locale Rlgrp = Rsemi + var one + var inv +
-  assumes lone: "one ** x = x"
-    and linv: "inv(x) ** x = one"
-
-lemma (in Rlgrp) 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
-
-locale Rrgrp = Rsemi + var one + var inv +
-  assumes rone: "x ** one = x"
-    and rinv: "x ** inv(x) = one"
-
-lemma (in Rrgrp) 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
-
-interpretation Rlgrp < Rrgrp
-  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! Rlgrp
-
-(* use of derived theorem *)
-
-lemma (in Rlgrp)
-  "y ** x = z ** x <-> y = z"
-  apply (rule rcancel)
-  print_interps Rrgrp thm lcancel rcancel
-  done
-
-(* circular interpretation *)
-
-interpretation Rrgrp < Rlgrp
-  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! Rrgrp
-print_locale! Rlgrp
-
-subsection {* Interaction of Interpretation in Theories and Locales:
-  in Locale, then in Theory *}
-
-consts
-  rone :: i
-  rinv :: "i => i"
-
-axioms
-  r_one : "rone # x = x"
-  r_inv : "rinv(x) # x = rone"
-
-interpretation Rbool: Rlgrp ["op #" "rone" "rinv"]
-proof
-  fix x y z
-  {
-    show "(x # y) # z = x # (y # z)" by (rule i_assoc)
-  next
-    show "rone # x = x" by (rule r_one)
-  next
-    show "rinv(x) # x = rone" by (rule r_inv)
-  }
-qed
-
-(* derived elements *)
-
-print_interps Rrgrp
-print_interps Rlgrp
-
-lemma "y # x = z # x <-> y = z" by (rule Rbool.rcancel)
-
-(* adding lemma to derived element *)
-
-lemma (in Rrgrp) new_cancel:
-  "b ** a = c ** a <-> b = c"
-  by (rule rcancel)
-
-thm Rbool.new_cancel (* additional prems discharged!! *)
-
-ML {* check_thm "Rbool.new_cancel" *}
-
-lemma "b # a = c # a <-> b = c" by (rule Rbool.new_cancel)
-
-
-subsection {* Interaction of Interpretation in Theories and Locales:
-  in Theory, then in Locale *}
-
-(* Another copy of the group example *)
-
-locale Rqsemi = var prod (infixl "**" 65) +
-  assumes assoc: "(x ** y) ** z = x ** (y ** z)"
-
-locale Rqlgrp = Rqsemi + var one + var inv +
-  assumes lone: "one ** x = x"
-    and linv: "inv(x) ** x = one"
-
-lemma (in Rqlgrp) 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
-
-locale Rqrgrp = Rqsemi + var one + var inv +
-  assumes rone: "x ** one = x"
-    and rinv: "x ** inv(x) = one"
-
-lemma (in Rqrgrp) 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
-
-interpretation Rqrgrp < Rrgrp
-  apply unfold_locales
-  apply (rule assoc)
-  apply (rule rone)
-  apply (rule rinv)
-  done
-
-interpretation R2: Rqlgrp ["op #" "rone" "rinv"] 
-  apply unfold_locales  (* FIXME: unfold_locales is too eager and shouldn't
-                          solve this. *)
-  apply (rule i_assoc)
-  apply (rule r_one)
-  apply (rule r_inv)
-  done
-
-print_interps Rqsemi
-print_interps Rqlgrp
-print_interps Rlgrp  (* no interpretations yet *)
-
-
-interpretation Rqlgrp < Rqrgrp
-  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
-
-print_interps! Rqrgrp
-print_interps! Rsemi  (* witness must not have meta hyps *)
-print_interps! Rrgrp  (* witness must not have meta hyps *)
-print_interps! Rlgrp  (* witness must not have meta hyps *)
-thm R2.rcancel
-thm R2.lcancel
-
-ML {* check_thm "R2.rcancel"; check_thm "R2.lcancel" *}
-
-
-subsection {* Generation of Witness Theorems for Transitive Interpretations *}
-
-locale Rtriv = var x +
-  assumes x: "x = x"
-
-locale Rtriv2 = var x + var y +
-  assumes x: "x = x" and y: "y = y"
-
-interpretation Rtriv2 < Rtriv x
-  apply unfold_locales
-  apply (rule x)
-  done
-
-interpretation Rtriv2 < Rtriv y
-  apply unfold_locales
-  apply (rule y)
-  done
-
-print_locale Rtriv2
-
-locale Rtriv3 = var x + var y + var z +
-  assumes x: "x = x" and y: "y = y" and z: "z = z"
-
-interpretation Rtriv3 < Rtriv2 x y
-  apply unfold_locales
-  apply (rule x)
-  apply (rule y)
-  done
-
-print_locale Rtriv3
-
-interpretation Rtriv3 < Rtriv2 x z
-  apply unfold_locales
-  apply (rule x_y_z.x)
-  apply (rule z)
-  done
-
-ML {* set show_types *}
-
-print_locale Rtriv3
-
-
-subsection {* Normalisation Replaces Assumed Element by Derived Element *}
-
-typedecl ('a, 'b) pair
-arities pair :: ("term", "term") "term"
-
-consts
-  pair :: "['a, 'b] => ('a, 'b) pair"
-  fst :: "('a, 'b) pair => 'a"
-  snd :: "('a, 'b) pair => 'b"
-
-axioms
-  fst [simp]: "fst(pair(x, y)) = x"
-  snd [simp]: "snd(pair(x, y)) = y"
-
-locale Rpair = var prod (infixl "**" 65) + var prodP (infixl "***" 65) +
-  defines P_def: "x *** y == pair(fst(x) ** fst(y), snd(x) ** snd(y))"
-
-locale Rpair_semi = Rpair + Rsemi
-
-interpretation Rpair_semi < Rsemi prodP (infixl "***" 65)
-proof unfold_locales
-  fix x y z
-  show "(x *** y) *** z = x *** (y *** z)"
-    apply (simp only: P_def) apply (simp add: assoc) (* FIXME: unfold P_def fails *)
-    done
-qed
-
-locale Rsemi_rev = Rsemi + var rprod (infixl "++" 65) +
-  defines r_def: "x ++ y == y ** x"
-
-lemma (in Rsemi_rev) r_assoc:
-  "(x ++ y) ++ z = x ++ (y ++ z)"
-  by (simp add: r_def assoc)
-
-
-subsection {* Import of Locales with Predicates as Interpretation *}
-
-locale Ra =
-  assumes Ra: "True"
-
-locale Rb = Ra +
-  assumes Rb: "True"
-
-locale Rc = Rb +
-  assumes Rc: "True"
-
-print_locale! Rc
-
-
-section {* Interpretation of Defined Concepts *}
-
-text {* Naming convention for global objects: prefixes D and d *}
-
-
-subsection {* Simple examples *}
-
-locale Da = fixes a :: o
-  assumes true: a
-
-text {* In the following examples, @{term "~ a"} is the defined concept. *}
-
-lemma (in Da) not_false: "~ a <-> False"
-  apply simp apply (rule true) done
-
-interpretation D1: Da ["True"]
-  where "~ True == False"
-  apply -
-  apply unfold_locales [1] apply rule
-  by simp
-
-thm D1.not_false
-lemma "False <-> False" apply (rule D1.not_false) done
-
-interpretation D2: Da ["x | ~ x"]
-  where "~ (x | ~ x) <-> ~ x & x"
-  apply -
-  apply unfold_locales [1] apply fast
-  by simp
-
-thm D2.not_false
-lemma "~ x & x <-> False" apply (rule D2.not_false) done
-
-print_interps! Da
-
-(* Subscriptions of interpretations *)
-
-lemma (in Da) not_false2: "~a <-> False"
-  apply simp apply (rule true) done
-
-thm D1.not_false2 D2.not_false2
-lemma "False <-> False" apply (rule D1.not_false2) done
-lemma "~x & x <-> False" apply (rule D2.not_false2) done
-
-(* Unfolding in attributes *)
-
-locale Db = Da +
-  fixes b :: o
-  assumes a_iff_b: "~a <-> b"
-
-lemmas (in Db) not_false_b = not_false [unfolded a_iff_b]
-
-interpretation D2: Db ["x | ~ x" "~ (x <-> x)"]
-  apply unfold_locales apply fast done
-
-thm D2.not_false_b
-lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b) done
-
-(* Subscription and attributes *)
-
-lemmas (in Db) not_false_b2 = not_false [unfolded a_iff_b]
-
-thm D2.not_false_b2
-lemma "~(x <-> x) <-> False" apply (rule D2.not_false_b2) done
-
-end

--- a/src/FOL/ex/NewLocaleTest.thy	Fri Dec 19 15:05:37 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Fri Dec 19 16:39:23 2008 +0100
@@ -8,7 +8,6 @@
 imports NewLocaleSetup
 begin
 
-ML_val {* set new_locales *}
 ML_val {* set Toplevel.debug *}
 
 

--- a/src/FOL/ex/ROOT.ML	Fri Dec 19 15:05:37 2008 +0100
+++ b/src/FOL/ex/ROOT.ML	Fri Dec 19 16:39:23 2008 +0100
@@ -29,6 +29,5 @@
 ];
 
 (*regression test for locales -- sets several global flags!*)
-no_document use_thy "LocaleTest";
 no_document use_thy "NewLocaleTest";
 

--- a/src/HOL/ROOT.ML	Fri Dec 19 15:05:37 2008 +0100
+++ b/src/HOL/ROOT.ML	Fri Dec 19 16:39:23 2008 +0100
@@ -3,7 +3,6 @@
 Classical Higher-order Logic -- batteries included.
 *)
 
-set new_locales;
 use_thy "Complex_Main";
 
 val HOL_proofs = ! Proofterm.proofs;

--- a/src/HOL/main.ML	Fri Dec 19 15:05:37 2008 +0100
+++ b/src/HOL/main.ML	Fri Dec 19 16:39:23 2008 +0100
@@ -4,5 +4,4 @@
 Classical Higher-order Logic -- only "Main".
 *)
 
-set new_locales;
 use_thy "Main";

--- a/src/HOL/plain.ML	Fri Dec 19 15:05:37 2008 +0100
+++ b/src/HOL/plain.ML	Fri Dec 19 16:39:23 2008 +0100
@@ -3,5 +3,4 @@
 Classical Higher-order Logic -- plain Tool bootstrap.
 *)
 
-set new_locales;
 use_thy "Plain";

--- a/src/Pure/Isar/ROOT.ML	Fri Dec 19 15:05:37 2008 +0100
+++ b/src/Pure/Isar/ROOT.ML	Fri Dec 19 16:39:23 2008 +0100
@@ -51,7 +51,6 @@
 use "obtain.ML";
 
 (*local theories and targets*)
-val new_locales = ref false;
 use "local_theory.ML";
 use "overloading.ML";
 use "locale.ML";

--- a/src/Pure/Isar/specification.ML	Fri Dec 19 15:05:37 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Fri Dec 19 16:39:23 2008 +0100
@@ -59,18 +59,6 @@
 structure Specification: SPECIFICATION =
 struct
 
-(* new locales *)
-
-fun cert_stmt body concl ctxt =
-  let val (_, _, ctxt', concl') = Locale.cert_context_statement NONE body concl ctxt
-  in (concl', ctxt') end;
-fun read_stmt body concl ctxt =
-  let val (_, _, ctxt', concl') = Locale.read_context_statement NONE body concl ctxt
-  in (concl', ctxt') end;
-  
-fun cert_context_statement x = if !new_locales then Expression.cert_statement x else cert_stmt x;
-fun read_context_statement x = if !new_locales then Expression.read_statement x else read_stmt x;
-
 (* diagnostics *)
 
 fun print_consts _ _ [] = ()
@@ -370,8 +358,8 @@
 
 in
 
-val theorem = gen_theorem (K I) cert_context_statement;
-val theorem_cmd = gen_theorem Attrib.intern_src read_context_statement;
+val theorem = gen_theorem (K I) Expression.cert_statement;
+val theorem_cmd = gen_theorem Attrib.intern_src Expression.read_statement;
 
 fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
 

--- a/src/Pure/Isar/theory_target.ML	Fri Dec 19 15:05:37 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Dec 19 16:39:23 2008 +0100
@@ -25,19 +25,19 @@
 (* new locales *)
 
 fun locale_extern new_locale x = 
-  if !new_locales andalso new_locale then NewLocale.extern x else Locale.extern x;
+  if new_locale then NewLocale.extern x else Locale.extern x;
 fun locale_add_type_syntax new_locale x =
-  if !new_locales andalso new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
+  if new_locale then NewLocale.add_type_syntax x else Locale.add_type_syntax x;
 fun locale_add_term_syntax new_locale x =
-  if !new_locales andalso new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
+  if new_locale then NewLocale.add_term_syntax x else Locale.add_term_syntax x;
 fun locale_add_declaration new_locale x =
-  if !new_locales andalso new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
+  if new_locale then NewLocale.add_declaration x else Locale.add_declaration x;
 fun locale_add_thmss new_locale x =
-  if !new_locales andalso new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
+  if new_locale then NewLocale.add_thmss x else Locale.add_thmss x;
 fun locale_init new_locale x =
-  if !new_locales andalso new_locale then NewLocale.init x else Locale.init x;
+  if new_locale then NewLocale.init x else Locale.init x;
 fun locale_intern new_locale x =
-  if !new_locales andalso new_locale then NewLocale.intern x else Locale.intern x;
+  if new_locale then NewLocale.intern x else Locale.intern x;
 
 (* context data *)
 

--- a/src/ZF/ROOT.ML	Fri Dec 19 15:05:37 2008 +0100
+++ b/src/ZF/ROOT.ML	Fri Dec 19 16:39:23 2008 +0100
@@ -8,6 +8,5 @@
 Paulson.
 *)
 
-set new_locales;
 use_thys ["Main", "Main_ZFC"];