tuned unfold_locales invocation
authorhaftmann
Mon Nov 17 17:00:55 2008 +0100 (2008-11-17)
changeset 28823dcbef866c9e2
parent 28822 7ca11ecbc4fb
child 28824 1db25e5703e3
tuned unfold_locales invocation
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Module.thy
src/HOL/Algebra/Ring.thy
src/HOL/Algebra/RingHom.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/Groebner_Basis.thy
src/HOL/Hyperreal/FrechetDeriv.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Lattices.thy
src/HOL/Library/Countable.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Univ_Poly.thy
src/HOL/List.thy
src/HOL/NSA/Filter.thy
src/HOL/Nat.thy
src/HOL/OrderedGroup.thy
src/HOL/Orderings.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/RealVector.thy
src/HOL/Ring_and_Field.thy
src/HOL/Word/WordArith.thy
src/HOL/ex/LocaleTest2.thy
src/HOL/ex/Numeral.thy
src/HOL/ex/Tarski.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Mon Nov 17 17:00:27 2008 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Mon Nov 17 17:00:55 2008 +0100
     1.3 @@ -234,7 +234,7 @@
     1.4    by (rule a_normal)
     1.5  
     1.6    show "abelian_subgroup H G"
     1.7 -  by (unfold_locales, simp add: a_comm)
     1.8 +  proof qed (simp add: a_comm)
     1.9  qed
    1.10  
    1.11  lemma abelian_subgroupI2:
    1.12 @@ -549,7 +549,7 @@
    1.13  
    1.14  lemma (in abelian_group_hom) is_abelian_group_hom:
    1.15    "abelian_group_hom G H h"
    1.16 -by (unfold_locales)
    1.17 +  ..
    1.18  
    1.19  lemma (in abelian_group_hom) hom_add [simp]:
    1.20    "[| x : carrier G; y : carrier G |]
     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Mon Nov 17 17:00:27 2008 +0100
     2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Mon Nov 17 17:00:55 2008 +0100
     2.3 @@ -26,14 +26,14 @@
     2.4        and r_cancel: 
     2.5            "\<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"
     2.6    shows "monoid_cancel G"
     2.7 -by unfold_locales fact+
     2.8 +  proof qed fact+
     2.9  
    2.10  lemma (in monoid_cancel) is_monoid_cancel:
    2.11    "monoid_cancel G"
    2.12 -by intro_locales
    2.13 +  ..
    2.14  
    2.15  interpretation group \<subseteq> monoid_cancel
    2.16 -by unfold_locales simp+
    2.17 +  proof qed simp+
    2.18  
    2.19  
    2.20  locale comm_monoid_cancel = monoid_cancel + comm_monoid
    2.21 @@ -57,10 +57,10 @@
    2.22  
    2.23  lemma (in comm_monoid_cancel) is_comm_monoid_cancel:
    2.24    "comm_monoid_cancel G"
    2.25 -by intro_locales
    2.26 +  by intro_locales
    2.27  
    2.28  interpretation comm_group \<subseteq> comm_monoid_cancel
    2.29 -by unfold_locales
    2.30 +  ..
    2.31  
    2.32  
    2.33  subsection {* Products of Units in Monoids *}
    2.34 @@ -1839,7 +1839,7 @@
    2.35            "\<And>a fs fs'. \<lbrakk>a \<in> carrier G; set fs \<subseteq> carrier G; set fs' \<subseteq> carrier G; 
    2.36                         wfactors G fs a; wfactors G fs' a\<rbrakk> \<Longrightarrow> essentially_equal G fs fs'"
    2.37    shows "factorial_monoid G"
    2.38 -proof (unfold_locales)
    2.39 +proof
    2.40    fix a
    2.41    assume acarr: "a \<in> carrier G" and anunit: "a \<notin> Units G"
    2.42  
    2.43 @@ -3855,19 +3855,19 @@
    2.44  qed
    2.45  
    2.46  interpretation factorial_monoid \<subseteq> primeness_condition_monoid
    2.47 -  by (unfold_locales, rule irreducible_is_prime)
    2.48 +  proof qed (rule irreducible_is_prime)
    2.49  
    2.50  
    2.51  lemma (in factorial_monoid) primeness_condition:
    2.52    shows "primeness_condition_monoid G"
    2.53 -by unfold_locales
    2.54 +  ..
    2.55  
    2.56  lemma (in factorial_monoid) gcd_condition [simp]:
    2.57    shows "gcd_condition_monoid G"
    2.58 -by (unfold_locales, rule gcdof_exists)
    2.59 +  proof qed (rule gcdof_exists)
    2.60  
    2.61  interpretation factorial_monoid \<subseteq> gcd_condition_monoid
    2.62 -  by (unfold_locales, rule gcdof_exists)
    2.63 +  proof qed (rule gcdof_exists)
    2.64  
    2.65  lemma (in factorial_monoid) division_weak_lattice [simp]:
    2.66    shows "weak_lattice (division_rel G)"
     3.1 --- a/src/HOL/Algebra/Group.thy	Mon Nov 17 17:00:27 2008 +0100
     3.2 +++ b/src/HOL/Algebra/Group.thy	Mon Nov 17 17:00:55 2008 +0100
     3.3 @@ -6,7 +6,9 @@
     3.4  Based on work by Florian Kammueller, L C Paulson and Markus Wenzel.
     3.5  *)
     3.6  
     3.7 -theory Group imports FuncSet Lattice begin
     3.8 +theory Group
     3.9 +imports Lattice FuncSet
    3.10 +begin
    3.11  
    3.12  
    3.13  section {* Monoids and Groups *}
    3.14 @@ -280,7 +282,7 @@
    3.15    qed
    3.16    then have carrier_subset_Units: "carrier G <= Units G"
    3.17      by (unfold Units_def) fast
    3.18 -  show ?thesis by unfold_locales (auto simp: r_one m_assoc carrier_subset_Units)
    3.19 +  show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units)
    3.20  qed
    3.21  
    3.22  lemma (in monoid) group_l_invI:
    3.23 @@ -685,7 +687,7 @@
    3.24    assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
    3.25        x \<otimes> y = y \<otimes> x"
    3.26    shows "comm_group G"
    3.27 -  by unfold_locales (simp_all add: m_comm)
    3.28 +  proof qed (simp_all add: m_comm)
    3.29  
    3.30  lemma comm_groupI:
    3.31    fixes G (structure)
    3.32 @@ -713,7 +715,7 @@
    3.33  
    3.34  theorem (in group) subgroups_partial_order:
    3.35    "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
    3.36 -  by unfold_locales simp_all
    3.37 +  proof qed simp_all
    3.38  
    3.39  lemma (in group) subgroup_self:
    3.40    "subgroup (carrier G) G"
     4.1 --- a/src/HOL/Algebra/IntRing.thy	Mon Nov 17 17:00:27 2008 +0100
     4.2 +++ b/src/HOL/Algebra/IntRing.thy	Mon Nov 17 17:00:55 2008 +0100
     4.3 @@ -5,7 +5,7 @@
     4.4  *)
     4.5  
     4.6  theory IntRing
     4.7 -imports QuotRing Int Primes
     4.8 +imports QuotRing Lattice Int Primes
     4.9  begin
    4.10  
    4.11  
    4.12 @@ -104,7 +104,7 @@
    4.13      and "pow \<Z> x n = x^n"
    4.14  proof -
    4.15    -- "Specification"
    4.16 -  show "monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
    4.17 +  show "monoid \<Z>" proof qed (auto simp: int_ring_def)
    4.18    then interpret int: monoid ["\<Z>"] .
    4.19  
    4.20    -- "Carrier"
    4.21 @@ -121,7 +121,7 @@
    4.22    where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
    4.23  proof -
    4.24    -- "Specification"
    4.25 -  show "comm_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
    4.26 +  show "comm_monoid \<Z>" proof qed (auto simp: int_ring_def)
    4.27    then interpret int: comm_monoid ["\<Z>"] .
    4.28  
    4.29    -- "Operations"
    4.30 @@ -146,7 +146,7 @@
    4.31      and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
    4.32  proof -
    4.33    -- "Specification"
    4.34 -  show "abelian_monoid \<Z>" by (unfold_locales) (auto simp: int_ring_def)
    4.35 +  show "abelian_monoid \<Z>" proof qed (auto simp: int_ring_def)
    4.36    then interpret int: abelian_monoid ["\<Z>"] .
    4.37  
    4.38    -- "Operations"
    4.39 @@ -189,7 +189,7 @@
    4.40  qed
    4.41  
    4.42  interpretation int: "domain" ["\<Z>"]
    4.43 -  by (unfold_locales) (auto simp: int_ring_def left_distrib right_distrib)
    4.44 +  proof qed (auto simp: int_ring_def left_distrib right_distrib)
    4.45  
    4.46  
    4.47  text {* Removal of occurrences of @{term UNIV} in interpretation result
    4.48 @@ -211,7 +211,7 @@
    4.49      and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    4.50  proof -
    4.51    show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    4.52 -    by unfold_locales simp_all
    4.53 +    proof qed simp_all
    4.54    show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    4.55      by simp
    4.56    show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    4.57 @@ -248,7 +248,7 @@
    4.58  
    4.59  interpretation int (* [unfolded UNIV] *) :
    4.60    total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    4.61 -  by unfold_locales clarsimp
    4.62 +  proof qed clarsimp
    4.63  
    4.64  
    4.65  subsection {* Generated Ideals of @{text "\<Z>"} *}
     5.1 --- a/src/HOL/Algebra/Lattice.thy	Mon Nov 17 17:00:27 2008 +0100
     5.2 +++ b/src/HOL/Algebra/Lattice.thy	Mon Nov 17 17:00:55 2008 +0100
     5.3 @@ -916,12 +916,12 @@
     5.4  lemma (in weak_partial_order) weak_total_orderI:
     5.5    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
     5.6    shows "weak_total_order L"
     5.7 -  by unfold_locales (rule total)
     5.8 +  proof qed (rule total)
     5.9  
    5.10  text {* Total orders are lattices. *}
    5.11  
    5.12  interpretation weak_total_order < weak_lattice
    5.13 -proof unfold_locales
    5.14 +proof
    5.15    fix x y
    5.16    assume L: "x \<in> carrier L"  "y \<in> carrier L"
    5.17    show "EX s. least L s (Upper L {x, y})"
    5.18 @@ -980,7 +980,7 @@
    5.19      and inf_exists:
    5.20      "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    5.21    shows "weak_complete_lattice L"
    5.22 -  by unfold_locales (auto intro: sup_exists inf_exists)
    5.23 +  proof qed (auto intro: sup_exists inf_exists)
    5.24  
    5.25  constdefs (structure L)
    5.26    top :: "_ => 'a" ("\<top>\<index>")
    5.27 @@ -1106,12 +1106,6 @@
    5.28    shows "P"
    5.29    using assms unfolding lless_eq by auto
    5.30  
    5.31 -lemma lless_trans [trans]:
    5.32 -  assumes "a \<sqsubset> b" "b \<sqsubset> c"
    5.33 -    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
    5.34 -  shows "a \<sqsubset> c"
    5.35 -  using assms unfolding lless_eq by (blast dest: le_trans intro: sym)
    5.36 -
    5.37  end
    5.38  
    5.39  
    5.40 @@ -1133,14 +1127,14 @@
    5.41      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
    5.42  
    5.43  interpretation upper_semilattice < weak_upper_semilattice
    5.44 -  by unfold_locales (rule sup_of_two_exists)
    5.45 +  proof qed (rule sup_of_two_exists)
    5.46  
    5.47  locale lower_semilattice = partial_order +
    5.48    assumes inf_of_two_exists:
    5.49      "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
    5.50  
    5.51  interpretation lower_semilattice < weak_lower_semilattice
    5.52 -  by unfold_locales (rule inf_of_two_exists)
    5.53 +  proof qed (rule inf_of_two_exists)
    5.54  
    5.55  locale lattice = upper_semilattice + lower_semilattice
    5.56  
    5.57 @@ -1188,22 +1182,22 @@
    5.58  text {* Total Orders *}
    5.59  
    5.60  locale total_order = partial_order +
    5.61 -  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
    5.62 +  assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
    5.63  
    5.64  interpretation total_order < weak_total_order
    5.65 -  by unfold_locales (rule total)
    5.66 +  proof qed (rule total_order_total)
    5.67  
    5.68  text {* Introduction rule: the usual definition of total order *}
    5.69  
    5.70  lemma (in partial_order) total_orderI:
    5.71    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
    5.72    shows "total_order L"
    5.73 -  by unfold_locales (rule total)
    5.74 +  proof qed (rule total)
    5.75  
    5.76  text {* Total orders are lattices. *}
    5.77  
    5.78  interpretation total_order < lattice
    5.79 -  by unfold_locales (auto intro: sup_of_two_exists inf_of_two_exists)
    5.80 +  proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
    5.81  
    5.82  
    5.83  text {* Complete lattices *}
    5.84 @@ -1215,7 +1209,7 @@
    5.85      "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    5.86  
    5.87  interpretation complete_lattice < weak_complete_lattice
    5.88 -  by unfold_locales (auto intro: sup_exists inf_exists)
    5.89 +  proof qed (auto intro: sup_exists inf_exists)
    5.90  
    5.91  text {* Introduction rule: the usual definition of complete lattice *}
    5.92  
    5.93 @@ -1225,7 +1219,7 @@
    5.94      and inf_exists:
    5.95      "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
    5.96    shows "complete_lattice L"
    5.97 -  by unfold_locales (auto intro: sup_exists inf_exists)
    5.98 +  proof qed (auto intro: sup_exists inf_exists)
    5.99  
   5.100  theorem (in partial_order) complete_lattice_criterion1:
   5.101    assumes top_exists: "EX g. greatest L g (carrier L)"
   5.102 @@ -1282,7 +1276,7 @@
   5.103    (is "complete_lattice ?L")
   5.104  proof (rule partial_order.complete_latticeI)
   5.105    show "partial_order ?L"
   5.106 -    by unfold_locales auto
   5.107 +    proof qed auto
   5.108  next
   5.109    fix B
   5.110    assume B: "B \<subseteq> carrier ?L"
     6.1 --- a/src/HOL/Algebra/Module.thy	Mon Nov 17 17:00:27 2008 +0100
     6.2 +++ b/src/HOL/Algebra/Module.thy	Mon Nov 17 17:00:55 2008 +0100
     6.3 @@ -91,11 +91,11 @@
     6.4  
     6.5  lemma (in algebra) R_cring:
     6.6    "cring R"
     6.7 -  by unfold_locales
     6.8 +  ..
     6.9  
    6.10  lemma (in algebra) M_cring:
    6.11    "cring M"
    6.12 -  by unfold_locales
    6.13 +  ..
    6.14  
    6.15  lemma (in algebra) module:
    6.16    "module R M"
     7.1 --- a/src/HOL/Algebra/Ring.thy	Mon Nov 17 17:00:27 2008 +0100
     7.2 +++ b/src/HOL/Algebra/Ring.thy	Mon Nov 17 17:00:55 2008 +0100
     7.3 @@ -5,7 +5,8 @@
     7.4    Copyright: Clemens Ballarin
     7.5  *)
     7.6  
     7.7 -theory Ring imports FiniteProduct
     7.8 +theory Ring
     7.9 +imports FiniteProduct
    7.10  uses ("ringsimp.ML") begin
    7.11  
    7.12  
    7.13 @@ -188,7 +189,7 @@
    7.14  proof -
    7.15    interpret comm_group ["\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"]
    7.16      by (rule cg)
    7.17 -  show "abelian_group G" by (unfold_locales)
    7.18 +  show "abelian_group G" ..
    7.19  qed
    7.20  
    7.21  
    7.22 @@ -392,7 +393,7 @@
    7.23  
    7.24  lemma (in ring) is_abelian_group:
    7.25    "abelian_group R"
    7.26 -  by unfold_locales
    7.27 +  ..
    7.28  
    7.29  lemma (in ring) is_monoid:
    7.30    "monoid R"
    7.31 @@ -670,7 +671,7 @@
    7.32  lemma (in cring) cring_fieldI:
    7.33    assumes field_Units: "Units R = carrier R - {\<zero>}"
    7.34    shows "field R"
    7.35 -proof unfold_locales
    7.36 +proof
    7.37    from field_Units
    7.38    have a: "\<zero> \<notin> Units R" by fast
    7.39    have "\<one> \<in> Units R" by fast
     8.1 --- a/src/HOL/Algebra/RingHom.thy	Mon Nov 17 17:00:27 2008 +0100
     8.2 +++ b/src/HOL/Algebra/RingHom.thy	Mon Nov 17 17:00:55 2008 +0100
     8.3 @@ -17,7 +17,7 @@
     8.4      and hom_one [simp] = ring_hom_one [OF homh]
     8.5  
     8.6  interpretation ring_hom_cring \<subseteq> ring_hom_ring
     8.7 -  by (unfold_locales, rule homh)
     8.8 +  proof qed (rule homh)
     8.9  
    8.10  interpretation ring_hom_ring \<subseteq> abelian_group_hom R S
    8.11  apply (rule abelian_group_homI)
     9.1 --- a/src/HOL/Algebra/UnivPoly.thy	Mon Nov 17 17:00:27 2008 +0100
     9.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon Nov 17 17:00:55 2008 +0100
     9.3 @@ -7,7 +7,9 @@
     9.4  Contributions, in particular on long division, by Jesus Aransay.
     9.5  *)
     9.6  
     9.7 -theory UnivPoly imports Module RingHom begin
     9.8 +theory UnivPoly
     9.9 +imports Module RingHom
    9.10 +begin
    9.11  
    9.12  
    9.13  section {* Univariate Polynomials *}
    9.14 @@ -500,8 +502,7 @@
    9.15  *}
    9.16  
    9.17  lemma (in cring) cring:
    9.18 -  "cring R"
    9.19 -  by unfold_locales
    9.20 +  "cring R" ..
    9.21  
    9.22  lemma (in UP_cring) UP_algebra:
    9.23    "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
    9.24 @@ -1771,9 +1772,9 @@
    9.25    shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
    9.26    (is "eval R R id a ?g = _")
    9.27  proof -
    9.28 -  interpret UP_pre_univ_prop [R R id P] by unfold_locales simp
    9.29 +  interpret UP_pre_univ_prop [R R id P] proof qed simp
    9.30    have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
    9.31 -  interpret ring_hom_cring [P R "eval R R id a"] by unfold_locales (simp add: eval_ring_hom)
    9.32 +  interpret ring_hom_cring [P R "eval R R id a"] proof qed (simp add: eval_ring_hom)
    9.33    have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
    9.34      and mon0_closed: "monom P a 0 \<in> carrier P" 
    9.35      and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
    9.36 @@ -1818,7 +1819,7 @@
    9.37      and deg_r_0: "deg R r = 0"
    9.38      shows "r = monom P (eval R R id a f) 0"
    9.39  proof -
    9.40 -  interpret UP_pre_univ_prop [R R id P] by unfold_locales simp
    9.41 +  interpret UP_pre_univ_prop [R R id P] proof qed simp
    9.42    have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
    9.43      using eval_ring_hom [OF a] by simp
    9.44    have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
    9.45 @@ -1884,7 +1885,8 @@
    9.46    "UP INTEG"} globally.
    9.47  *}
    9.48  
    9.49 -interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id] using INTEG_id_eval by simp_all
    9.50 +interpretation INTEG: UP_pre_univ_prop [INTEG INTEG id]
    9.51 +  using INTEG_id_eval by simp_all
    9.52  
    9.53  lemma INTEG_closed [intro, simp]:
    9.54    "z \<in> carrier INTEG"
    10.1 --- a/src/HOL/Divides.thy	Mon Nov 17 17:00:27 2008 +0100
    10.2 +++ b/src/HOL/Divides.thy	Mon Nov 17 17:00:55 2008 +0100
    10.3 @@ -639,8 +639,8 @@
    10.4  
    10.5  text {* @{term "op dvd"} is a partial order *}
    10.6  
    10.7 -interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> n \<noteq> m"]
    10.8 -  by unfold_locales (auto intro: dvd_refl dvd_trans dvd_anti_sym)
    10.9 +interpretation dvd: order ["op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"]
   10.10 +  proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
   10.11  
   10.12  lemma dvd_diff: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
   10.13    unfolding dvd_def
    11.1 --- a/src/HOL/Finite_Set.thy	Mon Nov 17 17:00:27 2008 +0100
    11.2 +++ b/src/HOL/Finite_Set.thy	Mon Nov 17 17:00:55 2008 +0100
    11.3 @@ -21,7 +21,7 @@
    11.4    assumes "\<not> finite (UNIV :: 'a set)" and "finite A"
    11.5    shows "\<exists>a::'a. a \<notin> A"
    11.6  proof -
    11.7 -  from prems have "A \<noteq> UNIV" by blast
    11.8 +  from assms have "A \<noteq> UNIV" by blast
    11.9    thus ?thesis by blast
   11.10  qed
   11.11  
   11.12 @@ -833,7 +833,7 @@
   11.13  subsection {* Generalized summation over a set *}
   11.14  
   11.15  interpretation comm_monoid_add: comm_monoid_mult ["0::'a::comm_monoid_add" "op +"]
   11.16 -  by unfold_locales (auto intro: add_assoc add_commute)
   11.17 +  proof qed (auto intro: add_assoc add_commute)
   11.18  
   11.19  constdefs
   11.20    setsum :: "('a => 'b) => 'a set => 'b::comm_monoid_add"
   11.21 @@ -1727,7 +1727,7 @@
   11.22    case empty then show ?case by simp
   11.23  next
   11.24    interpret ab_semigroup_mult ["op Un"]
   11.25 -    by unfold_locales auto
   11.26 +    proof qed auto
   11.27    case insert 
   11.28    then show ?case by simp
   11.29  qed
   11.30 @@ -2125,11 +2125,7 @@
   11.31  
   11.32  lemma ab_semigroup_idem_mult_inf:
   11.33    "ab_semigroup_idem_mult inf"
   11.34 -  apply unfold_locales
   11.35 -  apply (rule inf_assoc)
   11.36 -  apply (rule inf_commute)
   11.37 -  apply (rule inf_idem)
   11.38 -  done
   11.39 +  proof qed (rule inf_assoc inf_commute inf_idem)+
   11.40  
   11.41  lemma below_fold1_iff:
   11.42    assumes "finite A" "A \<noteq> {}"
   11.43 @@ -2357,19 +2353,19 @@
   11.44  
   11.45  lemma ab_semigroup_idem_mult_min:
   11.46    "ab_semigroup_idem_mult min"
   11.47 -  by unfold_locales (auto simp add: min_def)
   11.48 +  proof qed (auto simp add: min_def)
   11.49  
   11.50  lemma ab_semigroup_idem_mult_max:
   11.51    "ab_semigroup_idem_mult max"
   11.52 -  by unfold_locales (auto simp add: max_def)
   11.53 +  proof qed (auto simp add: max_def)
   11.54  
   11.55  lemma min_lattice:
   11.56    "lower_semilattice (op \<le>) (op <) min"
   11.57 -  by unfold_locales (auto simp add: min_def)
   11.58 +  proof qed (auto simp add: min_def)
   11.59  
   11.60  lemma max_lattice:
   11.61    "lower_semilattice (op \<ge>) (op >) max"
   11.62 -  by unfold_locales (auto simp add: max_def)
   11.63 +  proof qed (auto simp add: max_def)
   11.64  
   11.65  lemma dual_max:
   11.66    "ord.max (op \<ge>) = min"
    12.1 --- a/src/HOL/Groebner_Basis.thy	Mon Nov 17 17:00:27 2008 +0100
    12.2 +++ b/src/HOL/Groebner_Basis.thy	Mon Nov 17 17:00:55 2008 +0100
    12.3 @@ -168,7 +168,7 @@
    12.4  
    12.5  interpretation class_semiring: gb_semiring
    12.6      ["op +" "op *" "op ^" "0::'a::{comm_semiring_1, recpower}" "1"]
    12.7 -  by unfold_locales (auto simp add: ring_simps power_Suc)
    12.8 +  proof qed (auto simp add: ring_simps power_Suc)
    12.9  
   12.10  lemmas nat_arith =
   12.11    add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
   12.12 @@ -244,7 +244,7 @@
   12.13  
   12.14  interpretation class_ring: gb_ring ["op +" "op *" "op ^"
   12.15      "0::'a::{comm_semiring_1,recpower,number_ring}" 1 "op -" "uminus"]
   12.16 -  by unfold_locales simp_all
   12.17 +  proof qed simp_all
   12.18  
   12.19  
   12.20  declaration {* normalizer_funs @{thm class_ring.gb_ring_axioms'} *}
    13.1 --- a/src/HOL/Hyperreal/FrechetDeriv.thy	Mon Nov 17 17:00:27 2008 +0100
    13.2 +++ b/src/HOL/Hyperreal/FrechetDeriv.thy	Mon Nov 17 17:00:55 2008 +0100
    13.3 @@ -31,7 +31,7 @@
    13.4  
    13.5  lemma bounded_linear_zero:
    13.6    "bounded_linear (\<lambda>x::'a::real_normed_vector. 0::'b::real_normed_vector)"
    13.7 -proof (unfold_locales)
    13.8 +proof
    13.9    show "(0::'b) = 0 + 0" by simp
   13.10    fix r show "(0::'b) = scaleR r 0" by simp
   13.11    have "\<forall>x::'a. norm (0::'b) \<le> norm x * 0" by simp
   13.12 @@ -43,7 +43,7 @@
   13.13  
   13.14  lemma bounded_linear_ident:
   13.15    "bounded_linear (\<lambda>x::'a::real_normed_vector. x)"
   13.16 -proof (unfold_locales)
   13.17 +proof
   13.18    fix x y :: 'a show "x + y = x + y" by simp
   13.19    fix r and x :: 'a show "scaleR r x = scaleR r x" by simp
   13.20    have "\<forall>x::'a. norm x \<le> norm x * 1" by simp
    14.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon Nov 17 17:00:27 2008 +0100
    14.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Mon Nov 17 17:00:55 2008 +0100
    14.3 @@ -935,7 +935,7 @@
    14.4  lemma real_CauchyI:
    14.5    assumes "Cauchy X"
    14.6    shows "real_Cauchy X"
    14.7 -by unfold_locales (fact assms)
    14.8 +  proof qed (fact assms)
    14.9  
   14.10  lemma (in real_Cauchy) mem_S: "\<forall>n\<ge>N. x < X n \<Longrightarrow> x \<in> S"
   14.11  by (unfold S_def, auto)
    15.1 --- a/src/HOL/Lattices.thy	Mon Nov 17 17:00:27 2008 +0100
    15.2 +++ b/src/HOL/Lattices.thy	Mon Nov 17 17:00:55 2008 +0100
    15.3 @@ -291,7 +291,7 @@
    15.4  
    15.5  lemma (in linorder) distrib_lattice_min_max:
    15.6    "distrib_lattice (op \<le>) (op <) min max"
    15.7 -proof unfold_locales
    15.8 +proof
    15.9    have aux: "\<And>x y \<Colon> 'a. x < y \<Longrightarrow> y \<le> x \<Longrightarrow> x = y"
   15.10      by (auto simp add: less_le antisym)
   15.11    fix x y z
    16.1 --- a/src/HOL/Library/Countable.thy	Mon Nov 17 17:00:27 2008 +0100
    16.2 +++ b/src/HOL/Library/Countable.thy	Mon Nov 17 17:00:55 2008 +0100
    16.3 @@ -49,7 +49,7 @@
    16.4    by (rule countable_classI [of "id"]) simp 
    16.5  
    16.6  subclass (in finite) countable
    16.7 -proof unfold_locales
    16.8 +proof
    16.9    have "finite (UNIV\<Colon>'a set)" by (rule finite_UNIV)
   16.10    with finite_conv_nat_seg_image [of UNIV]
   16.11    obtain n and f :: "nat \<Rightarrow> 'a" 
    17.1 --- a/src/HOL/Library/Multiset.thy	Mon Nov 17 17:00:27 2008 +0100
    17.2 +++ b/src/HOL/Library/Multiset.thy	Mon Nov 17 17:00:55 2008 +0100
    17.3 @@ -1085,11 +1085,11 @@
    17.4    mset_le_trans simp: mset_less_def)
    17.5  
    17.6  interpretation mset_order_cancel_semigroup:
    17.7 -    pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
    17.8 +  pordered_cancel_ab_semigroup_add ["op +" "op \<le>#" "op <#"]
    17.9  proof qed (erule mset_le_mono_add [OF mset_le_refl])
   17.10  
   17.11  interpretation mset_order_semigroup_cancel:
   17.12 -    pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
   17.13 +  pordered_ab_semigroup_add_imp_le ["op +" "op \<le>#" "op <#"]
   17.14  proof qed simp
   17.15  
   17.16  
   17.17 @@ -1437,7 +1437,7 @@
   17.18   "image_mset f = fold_mset (op + o single o f) {#}"
   17.19  
   17.20  interpretation image_left_comm: left_commutative ["op + o single o f"]
   17.21 -by (unfold_locales) (simp add:union_ac)
   17.22 +  proof qed (simp add:union_ac)
   17.23  
   17.24  lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
   17.25  by (simp add: image_mset_def)
    18.1 --- a/src/HOL/Library/Univ_Poly.thy	Mon Nov 17 17:00:27 2008 +0100
    18.2 +++ b/src/HOL/Library/Univ_Poly.thy	Mon Nov 17 17:00:55 2008 +0100
    18.3 @@ -173,15 +173,15 @@
    18.4  class recpower_semiring_0 = semiring_0 + recpower
    18.5  class recpower_ring = ring + recpower
    18.6  class recpower_ring_1 = ring_1 + recpower
    18.7 -subclass (in recpower_ring_1) recpower_ring by unfold_locales
    18.8 +subclass (in recpower_ring_1) recpower_ring ..
    18.9  class recpower_comm_semiring_1 = recpower + comm_semiring_1
   18.10  class recpower_comm_ring_1 = recpower + comm_ring_1
   18.11 -subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 by unfold_locales
   18.12 +subclass (in recpower_comm_ring_1) recpower_comm_semiring_1 ..
   18.13  class recpower_idom = recpower + idom
   18.14 -subclass (in recpower_idom) recpower_comm_ring_1 by unfold_locales
   18.15 +subclass (in recpower_idom) recpower_comm_ring_1 ..
   18.16  class idom_char_0 = idom + ring_char_0
   18.17  class recpower_idom_char_0 = recpower + idom_char_0
   18.18 -subclass (in recpower_idom_char_0) recpower_idom by unfold_locales
   18.19 +subclass (in recpower_idom_char_0) recpower_idom ..
   18.20  
   18.21  lemma (in recpower_comm_ring_1) poly_exp: "poly (p %^ n) x = (poly p x) ^ n"
   18.22  apply (induct "n")
   18.23 @@ -429,7 +429,7 @@
   18.24  lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
   18.25  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])
   18.26  
   18.27 -subclass (in idom_char_0) comm_ring_1 by unfold_locales
   18.28 +subclass (in idom_char_0) comm_ring_1 ..
   18.29  lemma (in idom_char_0) poly_mult_left_cancel: "(poly (p *** q) = poly (p *** r)) = (poly p = poly [] | poly q = poly r)"
   18.30  proof-
   18.31    have "poly (p *** q) = poly (p *** r) \<longleftrightarrow> poly (p *** q +++ -- (p *** r)) = poly []" by (simp only: poly_add_minus_zero_iff)
    19.1 --- a/src/HOL/List.thy	Mon Nov 17 17:00:27 2008 +0100
    19.2 +++ b/src/HOL/List.thy	Mon Nov 17 17:00:55 2008 +0100
    19.3 @@ -549,9 +549,9 @@
    19.4  by (induct xs) auto
    19.5  
    19.6  interpretation semigroup_append: semigroup_add ["op @"]
    19.7 -by unfold_locales simp
    19.8 +  proof qed simp
    19.9  interpretation monoid_append: monoid_add ["[]" "op @"]
   19.10 -by unfold_locales (simp+)
   19.11 +  proof qed simp+
   19.12  
   19.13  lemma append_is_Nil_conv [iff]: "(xs @ ys = []) = (xs = [] \<and> ys = [])"
   19.14  by (induct xs) auto
   19.15 @@ -3834,7 +3834,7 @@
   19.16    "map_filter f P xs = map f (filter P xs)"
   19.17  by (induct xs) auto
   19.18  
   19.19 -lemma lenght_remdups_length_unique [code inline]:
   19.20 +lemma length_remdups_length_unique [code inline]:
   19.21    "length (remdups xs) = length_unique xs"
   19.22    by (induct xs) simp_all
   19.23  
    20.1 --- a/src/HOL/NSA/Filter.thy	Mon Nov 17 17:00:27 2008 +0100
    20.2 +++ b/src/HOL/NSA/Filter.thy	Mon Nov 17 17:00:55 2008 +0100
    20.3 @@ -77,10 +77,9 @@
    20.4  apply (simp add: singleton)
    20.5  done
    20.6  
    20.7 -lemma (in freeultrafilter) filter: "filter F" by unfold_locales
    20.8 +lemma (in freeultrafilter) filter: "filter F" ..
    20.9  
   20.10 -lemma (in freeultrafilter) ultrafilter: "ultrafilter F"
   20.11 -  by unfold_locales
   20.12 +lemma (in freeultrafilter) ultrafilter: "ultrafilter F" ..
   20.13  
   20.14  
   20.15  subsection {* Collect properties *}
    21.1 --- a/src/HOL/Nat.thy	Mon Nov 17 17:00:27 2008 +0100
    21.2 +++ b/src/HOL/Nat.thy	Mon Nov 17 17:00:55 2008 +0100
    21.3 @@ -1233,7 +1233,7 @@
    21.4  text{*Every @{text ordered_semidom} has characteristic zero.*}
    21.5  
    21.6  subclass semiring_char_0
    21.7 -  by unfold_locales (simp add: eq_iff order_eq_iff)
    21.8 +  proof qed (simp add: eq_iff order_eq_iff)
    21.9  
   21.10  text{*Special cases where either operand is zero*}
   21.11  
    22.1 --- a/src/HOL/OrderedGroup.thy	Mon Nov 17 17:00:27 2008 +0100
    22.2 +++ b/src/HOL/OrderedGroup.thy	Mon Nov 17 17:00:55 2008 +0100
    22.3 @@ -83,7 +83,7 @@
    22.4  begin
    22.5  
    22.6  subclass monoid_add
    22.7 -  by unfold_locales (insert add_0, simp_all add: add_commute)
    22.8 +  proof qed (insert add_0, simp_all add: add_commute)
    22.9  
   22.10  end
   22.11  
   22.12 @@ -99,7 +99,7 @@
   22.13  begin
   22.14  
   22.15  subclass monoid_mult
   22.16 -  by unfold_locales (insert mult_1, simp_all add: mult_commute)
   22.17 +  proof qed (insert mult_1, simp_all add: mult_commute)
   22.18  
   22.19  end
   22.20  
   22.21 @@ -123,7 +123,7 @@
   22.22  begin
   22.23  
   22.24  subclass cancel_semigroup_add
   22.25 -proof unfold_locales
   22.26 +proof
   22.27    fix a b c :: 'a
   22.28    assume "a + b = a + c" 
   22.29    then show "b = c" by (rule add_imp_eq)
   22.30 @@ -248,10 +248,10 @@
   22.31  begin
   22.32  
   22.33  subclass group_add
   22.34 -  by unfold_locales (simp_all add: ab_left_minus ab_diff_minus)
   22.35 +  proof qed (simp_all add: ab_left_minus ab_diff_minus)
   22.36  
   22.37  subclass cancel_ab_semigroup_add
   22.38 -proof unfold_locales
   22.39 +proof
   22.40    fix a b c :: 'a
   22.41    assume "a + b = a + c"
   22.42    then have "- a + a + b = - a + a + c"
   22.43 @@ -490,7 +490,7 @@
   22.44  subclass pordered_cancel_ab_semigroup_add ..
   22.45  
   22.46  subclass pordered_ab_semigroup_add_imp_le
   22.47 -proof unfold_locales
   22.48 +proof
   22.49    fix a b c :: 'a
   22.50    assume "c + a \<le> c + b"
   22.51    hence "(-c) + (c + a) \<le> (-c) + (c + b)" by (rule add_left_mono)
   22.52 @@ -646,7 +646,7 @@
   22.53  subclass ordered_ab_semigroup_add ..
   22.54  
   22.55  subclass pordered_ab_semigroup_add_imp_le
   22.56 -proof unfold_locales
   22.57 +proof
   22.58    fix a b c :: 'a
   22.59    assume le: "c + a <= c + b"  
   22.60    show "a <= b"
   22.61 @@ -1243,7 +1243,7 @@
   22.62    have abs_leI: "\<And>a b. a \<le> b \<Longrightarrow> - a \<le> b \<Longrightarrow> \<bar>a\<bar> \<le> b"
   22.63      by (simp add: abs_lattice le_supI)
   22.64    show ?thesis
   22.65 -  proof unfold_locales
   22.66 +  proof
   22.67      fix a
   22.68      show "0 \<le> \<bar>a\<bar>" by simp
   22.69    next
    23.1 --- a/src/HOL/Orderings.thy	Mon Nov 17 17:00:27 2008 +0100
    23.2 +++ b/src/HOL/Orderings.thy	Mon Nov 17 17:00:55 2008 +0100
    23.3 @@ -71,7 +71,7 @@
    23.4  
    23.5  lemma dual_preorder:
    23.6    "preorder (op \<ge>) (op >)"
    23.7 -by unfold_locales (auto simp add: less_le_not_le intro: order_trans)
    23.8 +proof qed (auto simp add: less_le_not_le intro: order_trans)
    23.9  
   23.10  end
   23.11  
    24.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Nov 17 17:00:27 2008 +0100
    24.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Nov 17 17:00:55 2008 +0100
    24.3 @@ -369,8 +369,8 @@
    24.4    interpret subspace [F E] by fact
    24.5    interpret linearform [F f] by fact
    24.6    interpret continuous [F norm f] by fact
    24.7 -  have E: "vectorspace E" by unfold_locales
    24.8 -  have F: "vectorspace F" by rule unfold_locales
    24.9 +  have E: "vectorspace E" by intro_locales
   24.10 +  have F: "vectorspace F" by rule intro_locales
   24.11    have F_norm: "normed_vectorspace F norm"
   24.12      using FE E_norm by (rule subspace_normed_vs)
   24.13    have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
    25.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Nov 17 17:00:27 2008 +0100
    25.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Nov 17 17:00:55 2008 +0100
    25.3 @@ -109,7 +109,7 @@
    25.4    proof
    25.5      show "vectorspace F" by (rule vectorspace) unfold_locales
    25.6    next
    25.7 -    have "NormedSpace.norm E norm" by unfold_locales
    25.8 +    have "NormedSpace.norm E norm" ..
    25.9      with subset show "NormedSpace.norm F norm"
   25.10        by (simp add: norm_def seminorm_def norm_axioms_def)
   25.11    qed
    26.1 --- a/src/HOL/Real/RealVector.thy	Mon Nov 17 17:00:27 2008 +0100
    26.2 +++ b/src/HOL/Real/RealVector.thy	Mon Nov 17 17:00:55 2008 +0100
    26.3 @@ -62,7 +62,7 @@
    26.4    and scale_left_diff_distrib: "scale (a - b) x = scale a x - scale b x"
    26.5  proof -
    26.6    interpret s: additive ["\<lambda>a. scale a x"]
    26.7 -    by unfold_locales (rule scale_left_distrib)
    26.8 +    proof qed (rule scale_left_distrib)
    26.9    show "scale 0 x = 0" by (rule s.zero)
   26.10    show "scale (- a) x = - (scale a x)" by (rule s.minus)
   26.11    show "scale (a - b) x = scale a x - scale b x" by (rule s.diff)
   26.12 @@ -73,7 +73,7 @@
   26.13    and scale_right_diff_distrib: "scale a (x - y) = scale a x - scale a y"
   26.14  proof -
   26.15    interpret s: additive ["\<lambda>x. scale a x"]
   26.16 -    by unfold_locales (rule scale_right_distrib)
   26.17 +    proof qed (rule scale_right_distrib)
   26.18    show "scale a 0 = 0" by (rule s.zero)
   26.19    show "scale a (- x) = - (scale a x)" by (rule s.minus)
   26.20    show "scale a (x - y) = scale a x - scale a y" by (rule s.diff)
   26.21 @@ -197,10 +197,10 @@
   26.22  done
   26.23  
   26.24  interpretation scaleR_left: additive ["(\<lambda>a. scaleR a x::'a::real_vector)"]
   26.25 -by unfold_locales (rule scaleR_left_distrib)
   26.26 +proof qed (rule scaleR_left_distrib)
   26.27  
   26.28  interpretation scaleR_right: additive ["(\<lambda>x. scaleR a x::'a::real_vector)"]
   26.29 -by unfold_locales (rule scaleR_right_distrib)
   26.30 +proof qed (rule scaleR_right_distrib)
   26.31  
   26.32  lemma nonzero_inverse_scaleR_distrib:
   26.33    fixes x :: "'a::real_div_algebra" shows
    27.1 --- a/src/HOL/Ring_and_Field.thy	Mon Nov 17 17:00:27 2008 +0100
    27.2 +++ b/src/HOL/Ring_and_Field.thy	Mon Nov 17 17:00:55 2008 +0100
    27.3 @@ -45,7 +45,7 @@
    27.4  begin
    27.5  
    27.6  subclass semiring_0
    27.7 -proof unfold_locales
    27.8 +proof
    27.9    fix a :: 'a
   27.10    have "0 * a + 0 * a = 0 * a + 0"
   27.11      by (simp add: left_distrib [symmetric])
   27.12 @@ -66,7 +66,7 @@
   27.13  begin
   27.14  
   27.15  subclass semiring
   27.16 -proof unfold_locales
   27.17 +proof
   27.18    fix a b c :: 'a
   27.19    show "(a + b) * c = a * c + b * c" by (simp add: distrib)
   27.20    have "a * (b + c) = (b + c) * a" by (simp add: mult_ac)
   27.21 @@ -362,7 +362,7 @@
   27.22  begin
   27.23  
   27.24  subclass ring_1_no_zero_divisors
   27.25 -proof unfold_locales
   27.26 +proof
   27.27    fix a b :: 'a
   27.28    assume a: "a \<noteq> 0" and b: "b \<noteq> 0"
   27.29    show "a * b \<noteq> 0"
   27.30 @@ -476,7 +476,7 @@
   27.31  begin
   27.32  
   27.33  subclass division_ring
   27.34 -proof unfold_locales
   27.35 +proof
   27.36    fix a :: 'a
   27.37    assume "a \<noteq> 0"
   27.38    thus "inverse a * a = 1" by (rule field_inverse)
   27.39 @@ -595,7 +595,7 @@
   27.40  subclass semiring_0_cancel ..
   27.41  
   27.42  subclass ordered_semiring
   27.43 -proof unfold_locales
   27.44 +proof
   27.45    fix a b c :: 'a
   27.46    assume A: "a \<le> b" "0 \<le> c"
   27.47    from A show "c * a \<le> c * b"
   27.48 @@ -713,7 +713,7 @@
   27.49  begin
   27.50  
   27.51  subclass pordered_semiring
   27.52 -proof unfold_locales
   27.53 +proof
   27.54    fix a b c :: 'a
   27.55    assume "a \<le> b" "0 \<le> c"
   27.56    thus "c * a \<le> c * b" by (rule mult_mono1)
   27.57 @@ -736,7 +736,7 @@
   27.58  begin
   27.59  
   27.60  subclass ordered_semiring_strict
   27.61 -proof unfold_locales
   27.62 +proof
   27.63    fix a b c :: 'a
   27.64    assume "a < b" "0 < c"
   27.65    thus "c * a < c * b" by (rule mult_strict_left_mono_comm)
   27.66 @@ -744,7 +744,7 @@
   27.67  qed
   27.68  
   27.69  subclass pordered_cancel_comm_semiring
   27.70 -proof unfold_locales
   27.71 +proof
   27.72    fix a b c :: 'a
   27.73    assume "a \<le> b" "0 \<le> c"
   27.74    thus "c * a \<le> c * b"
   27.75 @@ -815,7 +815,7 @@
   27.76  subclass pordered_ring ..
   27.77  
   27.78  subclass pordered_ab_group_add_abs
   27.79 -proof unfold_locales
   27.80 +proof
   27.81    fix a b
   27.82    show "\<bar>a + b\<bar> \<le> \<bar>a\<bar> + \<bar>b\<bar>"
   27.83    by (auto simp add: abs_if not_less neg_less_eq_nonneg less_eq_neg_nonpos)
   27.84 @@ -852,7 +852,7 @@
   27.85    by (drule mult_strict_right_mono_neg, auto)
   27.86  
   27.87  subclass ring_no_zero_divisors
   27.88 -proof unfold_locales
   27.89 +proof
   27.90    fix a b
   27.91    assume "a \<noteq> 0" then have A: "a < 0 \<or> 0 < a" by (simp add: neq_iff)
   27.92    assume "b \<noteq> 0" then have B: "b < 0 \<or> 0 < b" by (simp add: neq_iff)
   27.93 @@ -1019,7 +1019,7 @@
   27.94  subclass idom ..
   27.95  
   27.96  subclass ordered_semidom
   27.97 -proof unfold_locales
   27.98 +proof
   27.99    have "0 \<le> 1 * 1" by (rule zero_le_square)
  27.100    thus "0 < 1" by (simp add: le_less)
  27.101  qed 
    28.1 --- a/src/HOL/Word/WordArith.thy	Mon Nov 17 17:00:27 2008 +0100
    28.2 +++ b/src/HOL/Word/WordArith.thy	Mon Nov 17 17:00:55 2008 +0100
    28.3 @@ -19,9 +19,8 @@
    28.4             simp: word_uint.Rep_inject [symmetric])
    28.5  
    28.6  lemma signed_linorder: "linorder word_sle word_sless"
    28.7 -  apply unfold_locales
    28.8 -      apply (unfold word_sle_def word_sless_def) 
    28.9 -  by auto 
   28.10 +proof
   28.11 +qed (unfold word_sle_def word_sless_def, auto)
   28.12  
   28.13  interpretation signed: linorder ["word_sle" "word_sless"] 
   28.14    by (rule signed_linorder)
    29.1 --- a/src/HOL/ex/LocaleTest2.thy	Mon Nov 17 17:00:27 2008 +0100
    29.2 +++ b/src/HOL/ex/LocaleTest2.thy	Mon Nov 17 17:00:55 2008 +0100
    29.3 @@ -435,7 +435,7 @@
    29.4  
    29.5  interpretation dlo < dlat
    29.6  (* TODO: definition syntax is unavailable *)
    29.7 -proof unfold_locales
    29.8 +proof
    29.9    fix x y
   29.10    from total have "is_inf x y (if x \<sqsubseteq> y then x else y)" by (auto simp: is_inf_def)
   29.11    then show "EX inf. is_inf x y inf" by blast
   29.12 @@ -446,7 +446,7 @@
   29.13  qed
   29.14  
   29.15  interpretation dlo < ddlat
   29.16 -proof unfold_locales
   29.17 +proof
   29.18    fix x y z
   29.19    show "x \<sqinter> (y \<squnion> z) = x \<sqinter> y \<squnion> x \<sqinter> z" (is "?l = ?r")
   29.20      txt {* Jacobson I, p.\ 462 *}
   29.21 @@ -475,7 +475,7 @@
   29.22    txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
   29.23  proof -
   29.24    show "dpo (op <= :: [int, int] => bool)"
   29.25 -    by unfold_locales auto
   29.26 +    proof qed auto
   29.27    then interpret int: dpo ["op <= :: [int, int] => bool"] .
   29.28      txt {* Gives interpreted version of @{text less_def} (without condition). *}
   29.29    show "(dpo.less (op <=) (x::int) y) = (x < y)"
   29.30 @@ -514,7 +514,7 @@
   29.31  qed
   29.32  
   29.33  interpretation int: dlo ["op <= :: [int, int] => bool"]
   29.34 -  by unfold_locales arith
   29.35 +  proof qed arith
   29.36  
   29.37  text {* Interpreted theorems from the locales, involving defined terms. *}
   29.38  
   29.39 @@ -531,7 +531,7 @@
   29.40    txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
   29.41  proof -
   29.42    show "dpo (op <= :: [nat, nat] => bool)"
   29.43 -    by unfold_locales auto
   29.44 +    proof qed auto
   29.45    then interpret nat: dpo ["op <= :: [nat, nat] => bool"] .
   29.46      txt {* Gives interpreted version of @{text less_def} (without condition). *}
   29.47    show "dpo.less (op <=) (x::nat) y = (x < y)"
   29.48 @@ -565,7 +565,7 @@
   29.49  qed
   29.50  
   29.51  interpretation nat: dlo ["op <= :: [nat, nat] => bool"]
   29.52 -  by unfold_locales arith
   29.53 +  proof qed arith
   29.54  
   29.55  text {* Interpreted theorems from the locales, involving defined terms. *}
   29.56  
   29.57 @@ -582,7 +582,7 @@
   29.58    txt {* We give interpretation for less, but not @{text is_inf} and @{text is_sub}. *}
   29.59  proof -
   29.60    show "dpo (op dvd :: [nat, nat] => bool)"
   29.61 -    by unfold_locales (auto simp: dvd_def)
   29.62 +    proof qed (auto simp: dvd_def)
   29.63    then interpret nat_dvd: dpo ["op dvd :: [nat, nat] => bool"] .
   29.64      txt {* Gives interpreted version of @{text less_def} (without condition). *}
   29.65    show "dpo.less (op dvd) (x::nat) y = (x dvd y & x ~= y)"
   29.66 @@ -842,7 +842,7 @@
   29.67    where "Dmonoid.unit (op o) id f = bij (f::'a => 'a)"
   29.68  (*    and "Dmonoid.inv (op o) id" = "inv :: ('a => 'a) => ('a => 'a)" *)
   29.69  proof -
   29.70 -  show "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
   29.71 +  show "Dmonoid op o (id :: 'a => 'a)" proof qed (simp_all add: o_assoc)
   29.72    note Dmonoid = this
   29.73  (*
   29.74    from this interpret Dmonoid ["op o" "id :: 'a => 'a"] .
   29.75 @@ -891,7 +891,7 @@
   29.76  interpretation Dfun: Dgrp ["op o" "id :: unit => unit"]
   29.77    where "Dmonoid.inv (op o) id f = inv (f :: unit => unit)"
   29.78  proof -
   29.79 -  have "Dmonoid op o (id :: 'a => 'a)" by unfold_locales (simp_all add: o_assoc)
   29.80 +  have "Dmonoid op o (id :: 'a => 'a)" ..
   29.81    note Dmonoid = this
   29.82  
   29.83    show "Dgrp (op o) (id :: unit => unit)"
    30.1 --- a/src/HOL/ex/Numeral.thy	Mon Nov 17 17:00:27 2008 +0100
    30.2 +++ b/src/HOL/ex/Numeral.thy	Mon Nov 17 17:00:55 2008 +0100
    30.3 @@ -699,7 +699,7 @@
    30.4  begin
    30.5  
    30.6  subclass semiring_1_minus
    30.7 -  by unfold_locales (simp_all add: ring_simps)
    30.8 +  proof qed (simp_all add: ring_simps)
    30.9  
   30.10  lemma Dig_zero_minus_of_num [numeral]:
   30.11    "0 - of_num n = - of_num n"
    31.1 --- a/src/HOL/ex/Tarski.thy	Mon Nov 17 17:00:27 2008 +0100
    31.2 +++ b/src/HOL/ex/Tarski.thy	Mon Nov 17 17:00:55 2008 +0100
    31.3 @@ -923,6 +923,6 @@
    31.4  apply (rule fixf_po, clarify)
    31.5  apply (simp add: P_def A_def r_def)
    31.6  apply (rule Tarski.tarski_full_lemma [OF Tarski.intro [OF _ Tarski_axioms.intro]])
    31.7 -proof - show "CLF cl f" by unfold_locales qed
    31.8 +proof - show "CLF cl f" .. qed
    31.9  
   31.10  end