# HG changeset patch
# User haftmann
# Date 1226937655 -3600
# Node ID dcbef866c9e2bc728a11d1c176019fc8b1f14cc1
# Parent  7ca11ecbc4fb6248b618905890eb18e91baa0cb2
tuned unfold_locales invocation

diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -234,7 +234,7 @@
   by (rule a_normal)
 
   show "abelian_subgroup H G"
-  by (unfold_locales, simp add: a_comm)
+  proof qed (simp add: a_comm)
 qed
 
 lemma abelian_subgroupI2:
@@ -549,7 +549,7 @@
 
 lemma (in abelian_group_hom) is_abelian_group_hom:
   "abelian_group_hom G H h"
-by (unfold_locales)
+  ..
 
 lemma (in abelian_group_hom) hom_add [simp]:
   "[| x : carrier G; y : carrier G |]
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -26,14 +26,14 @@
       and r_cancel: 
           "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
   shows "monoid_cancel G"
-by unfold_locales fact+
+  proof qed fact+
 
 lemma (in monoid_cancel) is_monoid_cancel:
   "monoid_cancel G"
-by intro_locales
+  ..
 
 interpretation group \<subseteq> monoid_cancel
-by unfold_locales simp+
+  proof qed simp+
 
 
 locale comm_monoid_cancel = monoid_cancel + comm_monoid
@@ -57,10 +57,10 @@
 
 lemma (in comm_monoid_cancel) is_comm_monoid_cancel:
   "comm_monoid_cancel G"
-by intro_locales
+  by intro_locales
 
 interpretation comm_group \<subseteq> comm_monoid_cancel
-by unfold_locales
+  ..
 
 
 subsection {* Products of Units in Monoids *}
@@ -1839,7 +1839,7 @@
           "\<And>a fs fs'. \<lbrakk>a \<in> carrier G; set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G; 
                        wfactors G fs a; wfactors G fs' a\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
   shows "factorial_monoid G"
-proof (unfold_locales)
+proof
   fix a
   assume acarr: "a \<in> carrier G" and anunit: "a \<notin> Units G"
 
@@ -3855,19 +3855,19 @@
 qed
 
 interpretation factorial_monoid \<subseteq> primeness_condition_monoid
-  by (unfold_locales, rule irreducible_is_prime)
+  proof qed (rule irreducible_is_prime)
 
 
 lemma (in factorial_monoid) primeness_condition:
   shows "primeness_condition_monoid G"
-by unfold_locales
+  ..
 
 lemma (in factorial_monoid) gcd_condition [simp]:
   shows "gcd_condition_monoid G"
-by (unfold_locales, rule gcdof_exists)
+  proof qed (rule gcdof_exists)
 
 interpretation factorial_monoid \<subseteq> gcd_condition_monoid
-  by (unfold_locales, rule gcdof_exists)
+  proof qed (rule gcdof_exists)
 
 lemma (in factorial_monoid) division_weak_lattice [simp]:
   shows "weak_lattice (division_rel G)"
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Group.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -6,7 +6,9 @@
 Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
 *)
 
-theory Group imports FuncSet Lattice begin
+theory Group
+imports Lattice FuncSet
+begin
 
 
 section {* Monoids and Groups *}
@@ -280,7 +282,7 @@
   qed
   then have carrier_subset_Units: "carrier G <= Units G"
     by (unfold Units_def) fast
-  show ?thesis by unfold_locales (auto simp: r_one m_assoc carrier_subset_Units)
+  show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units)
 qed
 
 lemma (in monoid) group_l_invI:
@@ -685,7 +687,7 @@
   assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
       x \<otimes> y = y \<otimes> x"
   shows "comm_group G"
-  by unfold_locales (simp_all add: m_comm)
+  proof qed (simp_all add: m_comm)
 
 lemma comm_groupI:
   fixes G (structure)
@@ -713,7 +715,7 @@
 
 theorem (in group) subgroups_partial_order:
   "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
-  by unfold_locales simp_all
+  proof qed simp_all
 
 lemma (in group) subgroup_self:
   "subgroup (carrier G) G"
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -5,7 +5,7 @@
 *)
 
 theory IntRing
-imports QuotRing Int Primes
+imports QuotRing Lattice Int Primes
 begin
 
 
@@ -104,7 +104,7 @@
     and "pow \<Z> x n = x^n"
 proof -
   -- "Specification"
-  show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+  show "monoid \<Z>" proof qed (auto simp: int_ring_def)
   then interpret int: monoid ["\<Z>"] .
 
   -- "Carrier"
@@ -121,7 +121,7 @@
   where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
 proof -
   -- "Specification"
-  show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+  show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
   then interpret int: comm_monoid ["\<Z>"] .
 
   -- "Operations"
@@ -146,7 +146,7 @@
     and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
 proof -
   -- "Specification"
-  show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
+  show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
   then interpret int: abelian_monoid ["\<Z>"] .
 
   -- "Operations"
@@ -189,7 +189,7 @@
 qed
 
 interpretation int: "domain" ["\<Z>"]
-  by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
+  proof qed (auto simp: int_ring_def left_distrib right_distrib)
 
 
 text {* Removal of occurrences of @{term UNIV} in interpretation result
@@ -211,7 +211,7 @@
     and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
 proof -
   show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
-    by unfold_locales simp_all
+    proof qed simp_all
   show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
     by simp
   show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
@@ -248,7 +248,7 @@
 
 interpretation int (* [unfolded UNIV] *) :
   total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
-  by unfold_locales clarsimp
+  proof qed clarsimp
 
 
 subsection {* Generated Ideals of @{text "\<Z>"} *}
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -916,12 +916,12 @@
 lemma (in weak_partial_order) weak_total_orderI:
   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   shows "weak_total_order L"
-  by unfold_locales (rule total)
+  proof qed (rule total)
 
 text {* Total orders are lattices. *}
 
 interpretation weak_total_order < weak_lattice
-proof unfold_locales
+proof
   fix x y
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   show "EX s. least L s (Upper L {x, y})"
@@ -980,7 +980,7 @@
     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "weak_complete_lattice L"
-  by unfold_locales (auto intro: sup_exists inf_exists)
+  proof qed (auto intro: sup_exists inf_exists)
 
 constdefs (structure L)
   top :: "_ => 'a" ("\<top>\<index>")
@@ -1106,12 +1106,6 @@
   shows "P"
   using assms unfolding lless_eq by auto
 
-lemma lless_trans [trans]:
-  assumes "a \<sqsubset> b" "b \<sqsubset> c"
-    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
-  shows "a \<sqsubset> c"
-  using assms unfolding lless_eq by (blast dest: le_trans intro: sym)
-
 end
 
 
@@ -1133,14 +1127,14 @@
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 
 interpretation upper_semilattice < weak_upper_semilattice
-  by unfold_locales (rule sup_of_two_exists)
+  proof qed (rule sup_of_two_exists)
 
 locale lower_semilattice = partial_order +
   assumes inf_of_two_exists:
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
 
 interpretation lower_semilattice < weak_lower_semilattice
-  by unfold_locales (rule inf_of_two_exists)
+  proof qed (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
 
@@ -1188,22 +1182,22 @@
 text {* Total Orders *}
 
 locale total_order = partial_order +
-  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
+  assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
 
 interpretation total_order < weak_total_order
-  by unfold_locales (rule total)
+  proof qed (rule total_order_total)
 
 text {* Introduction rule: the usual definition of total order *}
 
 lemma (in partial_order) total_orderI:
   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   shows "total_order L"
-  by unfold_locales (rule total)
+  proof qed (rule total)
 
 text {* Total orders are lattices. *}
 
 interpretation total_order < lattice
-  by unfold_locales (auto intro: sup_of_two_exists inf_of_two_exists)
+  proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
 text {* Complete lattices *}
@@ -1215,7 +1209,7 @@
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
 interpretation complete_lattice < weak_complete_lattice
-  by unfold_locales (auto intro: sup_exists inf_exists)
+  proof qed (auto intro: sup_exists inf_exists)
 
 text {* Introduction rule: the usual definition of complete lattice *}
 
@@ -1225,7 +1219,7 @@
     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "complete_lattice L"
-  by unfold_locales (auto intro: sup_exists inf_exists)
+  proof qed (auto intro: sup_exists inf_exists)
 
 theorem (in partial_order) complete_lattice_criterion1:
   assumes top_exists: "EX g. greatest L g (carrier L)"
@@ -1282,7 +1276,7 @@
   (is "complete_lattice ?L")
 proof (rule partial_order.complete_latticeI)
   show "partial_order ?L"
-    by unfold_locales auto
+    proof qed auto
 next
   fix B
   assume B: "B \<subseteq> carrier ?L"
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Module.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -91,11 +91,11 @@
 
 lemma (in algebra) R_cring:
   "cring R"
-  by unfold_locales
+  ..
 
 lemma (in algebra) M_cring:
   "cring M"
-  by unfold_locales
+  ..
 
 lemma (in algebra) module:
   "module R M"
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/Ring.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -5,7 +5,8 @@
   Copyright: Clemens Ballarin
 *)
 
-theory Ring imports FiniteProduct
+theory Ring
+imports FiniteProduct
 uses ("ringsimp.ML") begin
 
 
@@ -188,7 +189,7 @@
 proof -
   interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
     by (rule cg)
-  show "abelian_group G" by (unfold_locales)
+  show "abelian_group G" ..
 qed
 
 
@@ -392,7 +393,7 @@
 
 lemma (in ring) is_abelian_group:
   "abelian_group R"
-  by unfold_locales
+  ..
 
 lemma (in ring) is_monoid:
   "monoid R"
@@ -670,7 +671,7 @@
 lemma (in cring) cring_fieldI:
   assumes field_Units: "Units R = carrier R - {\<zero>}"
   shows "field R"
-proof unfold_locales
+proof
   from field_Units
   have a: "\<zero> \<notin> Units R" by fast
   have "\<one> \<in> Units R" by fast
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -17,7 +17,7 @@
     and hom_one [simp] = ring_hom_one [OF homh]
 
 interpretation ring_hom_cring \<subseteq> ring_hom_ring
-  by (unfold_locales, rule homh)
+  proof qed (rule homh)
 
 interpretation ring_hom_ring \<subseteq> abelian_group_hom R S
 apply (rule abelian_group_homI)
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -7,7 +7,9 @@
 Contributions, in particular on long division, by Jesus Aransay.
 *)
 
-theory UnivPoly imports Module RingHom begin
+theory UnivPoly
+imports Module RingHom
+begin
 
 
 section {* Univariate Polynomials *}
@@ -500,8 +502,7 @@
 *}
 
 lemma (in cring) cring:
-  "cring R"
-  by unfold_locales
+  "cring R" ..
 
 lemma (in UP_cring) UP_algebra:
   "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
@@ -1771,9 +1772,9 @@
   shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
   (is "eval R R id a ?g = _")
 proof -
-  interpret UP_pre_univ_prop [R R id P] by unfold_locales simp
+  interpret UP_pre_univ_prop [R R id P] proof qed simp
   have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
-  interpret ring_hom_cring [P R "eval R R id a"] by unfold_locales (simp add: eval_ring_hom)
+  interpret ring_hom_cring [P R "eval R R id a"] proof qed (simp add: eval_ring_hom)
   have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
     and mon0_closed: "monom P a 0 \<in> carrier P" 
     and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
@@ -1818,7 +1819,7 @@
     and deg_r_0: "deg R r = 0"
     shows "r = monom P (eval R R id a f) 0"
 proof -
-  interpret UP_pre_univ_prop [R R id P] by unfold_locales simp
+  interpret UP_pre_univ_prop [R R id P] proof qed simp
   have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
     using eval_ring_hom [OF a] by simp
   have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
@@ -1884,7 +1885,8 @@
   "UP INTEG"} globally.
 *}
 
-interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id] using INTEG_id_eval by simp_all
+interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
+  using INTEG_id_eval by simp_all
 
 lemma INTEG_closed [intro, simp]:
   "z \<in> carrier INTEG"
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Divides.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -639,8 +639,8 @@
 
 text {* @{term "op dvd"} is a partial order *}
 
-interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> n \<noteq> m"]
-  by unfold_locales (auto intro: dvd_refl dvd_trans dvd_anti_sym)
+interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
+  proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
 
 lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
   unfolding dvd_def
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -21,7 +21,7 @@
   assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
   shows "\<exists>a::'a. a \<notin> A"
 proof -
-  from prems have "A \<noteq> UNIV" by blast
+  from assms have "A \<noteq> UNIV" by blast
   thus ?thesis by blast
 qed
 
@@ -833,7 +833,7 @@
 subsection {* Generalized summation over a set *}
 
 interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
-  by unfold_locales (auto intro: add_assoc add_commute)
+  proof qed (auto intro: add_assoc add_commute)
 
 constdefs
   setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
@@ -1727,7 +1727,7 @@
   case empty then show ?case by simp
 next
   interpret ab_semigroup_mult ["op Un"]
-    by unfold_locales auto
+    proof qed auto
   case insert 
   then show ?case by simp
 qed
@@ -2125,11 +2125,7 @@
 
 lemma ab_semigroup_idem_mult_inf:
   "ab_semigroup_idem_mult inf"
-  apply unfold_locales
-  apply (rule inf_assoc)
-  apply (rule inf_commute)
-  apply (rule inf_idem)
-  done
+  proof qed (rule inf_assoc inf_commute inf_idem)+
 
 lemma below_fold1_iff:
   assumes "finite A" "A \<noteq> {}"
@@ -2357,19 +2353,19 @@
 
 lemma ab_semigroup_idem_mult_min:
   "ab_semigroup_idem_mult min"
-  by unfold_locales (auto simp add: min_def)
+  proof qed (auto simp add: min_def)
 
 lemma ab_semigroup_idem_mult_max:
   "ab_semigroup_idem_mult max"
-  by unfold_locales (auto simp add: max_def)
+  proof qed (auto simp add: max_def)
 
 lemma min_lattice:
   "lower_semilattice (op \<le>) (op <) min"
-  by unfold_locales (auto simp add: min_def)
+  proof qed (auto simp add: min_def)
 
 lemma max_lattice:
   "lower_semilattice (op \<ge>) (op >) max"
-  by unfold_locales (auto simp add: max_def)
+  proof qed (auto simp add: max_def)
 
 lemma dual_max:
   "ord.max (op \<ge>) = min"
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -168,7 +168,7 @@
 
 interpretation class_semiring: gb_semiring
     ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
-  by unfold_locales (auto simp add: ring_simps power_Suc)
+  proof qed (auto simp add: ring_simps power_Suc)
 
 lemmas nat_arith =
   add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
@@ -244,7 +244,7 @@
 
 interpretation class_ring: gb_ring ["op +" "op *" "op ^"
     "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
-  by unfold_locales simp_all
+  proof qed simp_all
 
 
 declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Hyperreal/FrechetDeriv.thy
--- a/src/HOL/Hyperreal/FrechetDeriv.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Hyperreal/FrechetDeriv.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -31,7 +31,7 @@
 
 lemma bounded_linear_zero:
   "bounded_linear (\<lambda>x::'a::real_normed_vector. 0::'b::real_normed_vector)"
-proof (unfold_locales)
+proof
   show "(0::'b) = 0 + 0" by simp
   fix r show "(0::'b) = scaleR r 0" by simp
   have "\<forall>x::'a. norm (0::'b) \<le> norm x * 0" by simp
@@ -43,7 +43,7 @@
 
 lemma bounded_linear_ident:
   "bounded_linear (\<lambda>x::'a::real_normed_vector. x)"
-proof (unfold_locales)
+proof
   fix x y :: 'a show "x + y = x + y" by simp
   fix r and x :: 'a show "scaleR r x = scaleR r x" by simp
   have "\<forall>x::'a. norm x \<le> norm x * 1" by simp
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -935,7 +935,7 @@
 lemma real_CauchyI:
   assumes "Cauchy X"
   shows "real_Cauchy X"
-by unfold_locales (fact assms)
+  proof qed (fact assms)
 
 lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S"
 by (unfold S_def, auto)
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Lattices.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -291,7 +291,7 @@
 
 lemma (in linorder) distrib_lattice_min_max:
   "distrib_lattice (op \<le>) (op <) min max"
-proof unfold_locales
+proof
   have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
     by (auto simp add: less_le antisym)
   fix x y z
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Library/Countable.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -49,7 +49,7 @@
   by (rule countable_classI [of "id"]) simp 
 
 subclass (in finite) countable
-proof unfold_locales
+proof
   have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
   with finite_conv_nat_seg_image [of UNIV]
   obtain n and f :: "nat \<Rightarrow> 'a" 
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -1085,11 +1085,11 @@
   mset_le_trans simp: mset_less_def)
 
 interpretation mset_order_cancel_semigroup:
-    pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
+  pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
 proof qed (erule mset_le_mono_add [OF mset_le_refl])
 
 interpretation mset_order_semigroup_cancel:
-    pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
+  pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
 proof qed simp
 
 
@@ -1437,7 +1437,7 @@
  "image_mset f = fold_mset (op + o single o f) {#}"
 
 interpretation image_left_comm: left_commutative ["op + o single o f"]
-by (unfold_locales) (simp add:union_ac)
+  proof qed (simp add:union_ac)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
 by (simp add: image_mset_def)
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Library/Univ_Poly.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -173,15 +173,15 @@
 class recpower_semiring_0 = semiring_0 + recpower
 class recpower_ring = ring + recpower
 class recpower_ring_1 = ring_1 + recpower
-subclass (in recpower_ring_1) recpower_ring by unfold_locales
+subclass (in recpower_ring_1) recpower_ring ..
 class recpower_comm_semiring_1 = recpower + comm_semiring_1
 class recpower_comm_ring_1 = recpower + comm_ring_1
-subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 by unfold_locales
+subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 ..
 class recpower_idom = recpower + idom
-subclass (in recpower_idom) recpower_comm_ring_1 by unfold_locales
+subclass (in recpower_idom) recpower_comm_ring_1 ..
 class idom_char_0 = idom + ring_char_0
 class recpower_idom_char_0 = recpower + idom_char_0
-subclass (in recpower_idom_char_0) recpower_idom by unfold_locales
+subclass (in recpower_idom_char_0) recpower_idom ..
 
 lemma (in recpower_comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
 apply (induct "n")
@@ -429,7 +429,7 @@
 lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
 by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib minus_mult_left[symmetric] minus_mult_right[symmetric])
 
-subclass (in idom_char_0) comm_ring_1 by unfold_locales
+subclass (in idom_char_0) comm_ring_1 ..
 lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
 proof-
   have "poly (p *** q) = poly (p *** r) \<longleftrightarrow> poly (p *** q +++ -- (p *** r)) = poly []" by (simp only: poly_add_minus_zero_iff)
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/List.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -549,9 +549,9 @@
 by (induct xs) auto
 
 interpretation semigroup_append: semigroup_add ["op @"]
-by unfold_locales simp
+  proof qed simp
 interpretation monoid_append: monoid_add ["[]" "op @"]
-by unfold_locales (simp+)
+  proof qed simp+
 
 lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
 by (induct xs) auto
@@ -3834,7 +3834,7 @@
   "map_filter f P xs = map f (filter P xs)"
 by (induct xs) auto
 
-lemma lenght_remdups_length_unique [code inline]:
+lemma length_remdups_length_unique [code inline]:
   "length (remdups xs) = length_unique xs"
   by (induct xs) simp_all
 
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/NSA/Filter.thy
--- a/src/HOL/NSA/Filter.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/NSA/Filter.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -77,10 +77,9 @@
 apply (simp add: singleton)
 done
 
-lemma (in freeultrafilter) filter: "filter F" by unfold_locales
+lemma (in freeultrafilter) filter: "filter F" ..
 
-lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
-  by unfold_locales
+lemma (in freeultrafilter) ultrafilter: "ultrafilter F" ..
 
 
 subsection {* Collect properties *}
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Nat.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -1233,7 +1233,7 @@
 text{*Every @{text ordered_semidom} has characteristic zero.*}
 
 subclass semiring_char_0
-  by unfold_locales (simp add: eq_iff order_eq_iff)
+  proof qed (simp add: eq_iff order_eq_iff)
 
 text{*Special cases where either operand is zero*}
 
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/OrderedGroup.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -83,7 +83,7 @@
 begin
 
 subclass monoid_add
-  by unfold_locales (insert add_0, simp_all add: add_commute)
+  proof qed (insert add_0, simp_all add: add_commute)
 
 end
 
@@ -99,7 +99,7 @@
 begin
 
 subclass monoid_mult
-  by unfold_locales (insert mult_1, simp_all add: mult_commute)
+  proof qed (insert mult_1, simp_all add: mult_commute)
 
 end
 
@@ -123,7 +123,7 @@
 begin
 
 subclass cancel_semigroup_add
-proof unfold_locales
+proof
   fix a b c :: 'a
   assume "a + b = a + c" 
   then show "b = c" by (rule add_imp_eq)
@@ -248,10 +248,10 @@
 begin
 
 subclass group_add
-  by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)
+  proof qed (simp_all add: ab_left_minus ab_diff_minus)
 
 subclass cancel_ab_semigroup_add
-proof unfold_locales
+proof
   fix a b c :: 'a
   assume "a + b = a + c"
   then have "- a + a + b = - a + a + c"
@@ -490,7 +490,7 @@
 subclass pordered_cancel_ab_semigroup_add ..
 
 subclass pordered_ab_semigroup_add_imp_le
-proof unfold_locales
+proof
   fix a b c :: 'a
   assume "c + a \<le> c + b"
   hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
@@ -646,7 +646,7 @@
 subclass ordered_ab_semigroup_add ..
 
 subclass pordered_ab_semigroup_add_imp_le
-proof unfold_locales
+proof
   fix a b c :: 'a
   assume le: "c + a <= c + b"  
   show "a <= b"
@@ -1243,7 +1243,7 @@
   have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
     by (simp add: abs_lattice le_supI)
   show ?thesis
-  proof unfold_locales
+  proof
     fix a
     show "0 \<le> \<bar>a\<bar>" by simp
   next
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Orderings.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -71,7 +71,7 @@
 
 lemma dual_preorder:
   "preorder (op \<ge>) (op >)"
-by unfold_locales (auto simp add: less_le_not_le intro: order_trans)
+proof qed (auto simp add: less_le_not_le intro: order_trans)
 
 end
 
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Real/HahnBanach/HahnBanach.thy
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -369,8 +369,8 @@
   interpret subspace [F E] by fact
   interpret linearform [F f] by fact
   interpret continuous [F norm f] by fact
-  have E: "vectorspace E" by unfold_locales
-  have F: "vectorspace F" by rule unfold_locales
+  have E: "vectorspace E" by intro_locales
+  have F: "vectorspace F" by rule intro_locales
   have F_norm: "normed_vectorspace F norm"
     using FE E_norm by (rule subspace_normed_vs)
   have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Real/HahnBanach/NormedSpace.thy
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -109,7 +109,7 @@
   proof
     show "vectorspace F" by (rule vectorspace) unfold_locales
   next
-    have "NormedSpace.norm E norm" by unfold_locales
+    have "NormedSpace.norm E norm" ..
     with subset show "NormedSpace.norm F norm"
       by (simp add: norm_def seminorm_def norm_axioms_def)
   qed
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Real/RealVector.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -62,7 +62,7 @@
   and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x"
 proof -
   interpret s: additive ["\<lambda>a. scale a x"]
-    by unfold_locales (rule scale_left_distrib)
+    proof qed (rule scale_left_distrib)
   show "scale 0 x = 0" by (rule s.zero)
   show "scale (- a) x = - (scale a x)" by (rule s.minus)
   show "scale (a - b) x = scale a x - scale b x" by (rule s.diff)
@@ -73,7 +73,7 @@
   and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y"
 proof -
   interpret s: additive ["\<lambda>x. scale a x"]
-    by unfold_locales (rule scale_right_distrib)
+    proof qed (rule scale_right_distrib)
   show "scale a 0 = 0" by (rule s.zero)
   show "scale a (- x) = - (scale a x)" by (rule s.minus)
   show "scale a (x - y) = scale a x - scale a y" by (rule s.diff)
@@ -197,10 +197,10 @@
 done
 
 interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
-by unfold_locales (rule scaleR_left_distrib)
+proof qed (rule scaleR_left_distrib)
 
 interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
-by unfold_locales (rule scaleR_right_distrib)
+proof qed (rule scaleR_right_distrib)
 
 lemma nonzero_inverse_scaleR_distrib:
   fixes x :: "'a::real_div_algebra" shows
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Ring_and_Field.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -45,7 +45,7 @@
 begin
 
 subclass semiring_0
-proof unfold_locales
+proof
   fix a :: 'a
   have "0 * a + 0 * a = 0 * a + 0"
     by (simp add: left_distrib [symmetric])
@@ -66,7 +66,7 @@
 begin
 
 subclass semiring
-proof unfold_locales
+proof
   fix a b c :: 'a
   show "(a + b) * c = a * c + b * c" by (simp add: distrib)
   have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
@@ -362,7 +362,7 @@
 begin
 
 subclass ring_1_no_zero_divisors
-proof unfold_locales
+proof
   fix a b :: 'a
   assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   show "a * b \<noteq> 0"
@@ -476,7 +476,7 @@
 begin
 
 subclass division_ring
-proof unfold_locales
+proof
   fix a :: 'a
   assume "a \<noteq> 0"
   thus "inverse a * a = 1" by (rule field_inverse)
@@ -595,7 +595,7 @@
 subclass semiring_0_cancel ..
 
 subclass ordered_semiring
-proof unfold_locales
+proof
   fix a b c :: 'a
   assume A: "a \<le> b" "0 \<le> c"
   from A show "c * a \<le> c * b"
@@ -713,7 +713,7 @@
 begin
 
 subclass pordered_semiring
-proof unfold_locales
+proof
   fix a b c :: 'a
   assume "a \<le> b" "0 \<le> c"
   thus "c * a \<le> c * b" by (rule mult_mono1)
@@ -736,7 +736,7 @@
 begin
 
 subclass ordered_semiring_strict
-proof unfold_locales
+proof
   fix a b c :: 'a
   assume "a < b" "0 < c"
   thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
@@ -744,7 +744,7 @@
 qed
 
 subclass pordered_cancel_comm_semiring
-proof unfold_locales
+proof
   fix a b c :: 'a
   assume "a \<le> b" "0 \<le> c"
   thus "c * a \<le> c * b"
@@ -815,7 +815,7 @@
 subclass pordered_ring ..
 
 subclass pordered_ab_group_add_abs
-proof unfold_locales
+proof
   fix a b
   show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
@@ -852,7 +852,7 @@
   by (drule mult_strict_right_mono_neg, auto)
 
 subclass ring_no_zero_divisors
-proof unfold_locales
+proof
   fix a b
   assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
   assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
@@ -1019,7 +1019,7 @@
 subclass idom ..
 
 subclass ordered_semidom
-proof unfold_locales
+proof
   have "0 \<le> 1 * 1" by (rule zero_le_square)
   thus "0 < 1" by (simp add: le_less)
 qed 
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Word/WordArith.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -19,9 +19,8 @@
            simp: word_uint.Rep_inject [symmetric])
 
 lemma signed_linorder: "linorder word_sle word_sless"
-  apply unfold_locales
-      apply (unfold word_sle_def word_sless_def) 
-  by auto 
+proof
+qed (unfold word_sle_def word_sless_def, auto)
 
 interpretation signed: linorder ["word_sle" "word_sless"] 
   by (rule signed_linorder)
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -435,7 +435,7 @@
 
 interpretation dlo < dlat
 (* TODO: definition syntax is unavailable *)
-proof unfold_locales
+proof
   fix x y
   from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
   then show "EX inf. is_inf x y inf" by blast
@@ -446,7 +446,7 @@
 qed
 
 interpretation dlo < ddlat
-proof unfold_locales
+proof
   fix x y z
   show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
     txt {* Jacobson I, p.\ 462 *}
@@ -475,7 +475,7 @@
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op <= :: [int, int] => bool)"
-    by unfold_locales auto
+    proof qed auto
   then interpret int: dpo ["op <= :: [int, int] => bool"] .
     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "(dpo.less (op <=) (x::int) y) = (x < y)"
@@ -514,7 +514,7 @@
 qed
 
 interpretation int: dlo ["op <= :: [int, int] => bool"]
-  by unfold_locales arith
+  proof qed arith
 
 text {* Interpreted theorems from the locales, involving defined terms. *}
 
@@ -531,7 +531,7 @@
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op <= :: [nat, nat] => bool)"
-    by unfold_locales auto
+    proof qed auto
   then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "dpo.less (op <=) (x::nat) y = (x < y)"
@@ -565,7 +565,7 @@
 qed
 
 interpretation nat: dlo ["op <= :: [nat, nat] => bool"]
-  by unfold_locales arith
+  proof qed arith
 
 text {* Interpreted theorems from the locales, involving defined terms. *}
 
@@ -582,7 +582,7 @@
   txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
 proof -
   show "dpo (op dvd :: [nat, nat] => bool)"
-    by unfold_locales (auto simp: dvd_def)
+    proof qed (auto simp: dvd_def)
   then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
     txt {* Gives interpreted version of @{text less_def} (without condition). *}
   show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
@@ -842,7 +842,7 @@
   where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
 (*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
 proof -
-  show "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
+  show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc)
   note Dmonoid = this
 (*
   from this interpret Dmonoid ["op o" "id :: 'a => 'a"] .
@@ -891,7 +891,7 @@
 interpretation Dfun: Dgrp ["op o" "id :: unit => unit"]
   where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
 proof -
-  have "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
+  have "Dmonoid op o (id :: 'a => 'a)" ..
   note Dmonoid = this
 
   show "Dgrp (op o) (id :: unit => unit)"
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/ex/Numeral.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -699,7 +699,7 @@
 begin
 
 subclass semiring_1_minus
-  by unfold_locales (simp_all add: ring_simps)
+  proof qed (simp_all add: ring_simps)
 
 lemma Dig_zero_minus_of_num [numeral]:
   "0 - of_num n = - of_num n"
diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/ex/Tarski.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -923,6 +923,6 @@
 apply (rule fixf_po, clarify)
 apply (simp add: P_def A_def r_def)
 apply (rule Tarski.tarski_full_lemma [OF Tarski.intro [OF _ Tarski_axioms.intro]])
-proof - show "CLF cl f" by unfold_locales qed
+proof - show "CLF cl f" .. qed
 
 end