# HG changeset patch
# User wenzelm
# Date 1314980265 -7200
# Node ID fe03653315667519fd9f54b81451a6e81a307e53
# Parent  d80fe56788a51d81ff428c5833a697a62d9a5a43
tuned proofs;

diff -r d80fe56788a5 -r fe0365331566 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Fri Sep 02 17:58:32 2011 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Fri Sep 02 18:17:45 2011 +0200
@@ -233,10 +233,10 @@
   shows "abelian_subgroup H G"
 proof -
   interpret normal "H" "\<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
-  by (rule a_normal)
+    by (rule a_normal)
 
   show "abelian_subgroup H G"
-  proof qed (simp add: a_comm)
+    by default (simp add: a_comm)
 qed
 
 lemma abelian_subgroupI2:
diff -r d80fe56788a5 -r fe0365331566 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Fri Sep 02 17:58:32 2011 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Fri Sep 02 18:17:45 2011 +0200
@@ -25,14 +25,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"
-  proof qed fact+
+    by default fact+
 
 lemma (in monoid_cancel) is_monoid_cancel:
   "monoid_cancel G"
   ..
 
 sublocale group \<subseteq> monoid_cancel
-  proof qed simp+
+  by default simp_all
 
 
 locale comm_monoid_cancel = monoid_cancel + comm_monoid
@@ -3655,7 +3655,7 @@
 done
 
 sublocale factorial_monoid \<subseteq> primeness_condition_monoid
-  proof qed (rule irreducible_is_prime)
+  by default (rule irreducible_is_prime)
 
 
 lemma (in factorial_monoid) primeness_condition:
@@ -3664,10 +3664,10 @@
 
 lemma (in factorial_monoid) gcd_condition [simp]:
   shows "gcd_condition_monoid G"
-  proof qed (rule gcdof_exists)
+  by default (rule gcdof_exists)
 
 sublocale factorial_monoid \<subseteq> gcd_condition_monoid
-  proof qed (rule gcdof_exists)
+  by default (rule gcdof_exists)
 
 lemma (in factorial_monoid) division_weak_lattice [simp]:
   shows "weak_lattice (division_rel G)"
diff -r d80fe56788a5 -r fe0365331566 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Fri Sep 02 17:58:32 2011 +0200
+++ b/src/HOL/Algebra/Group.thy	Fri Sep 02 18:17:45 2011 +0200
@@ -286,7 +286,7 @@
   qed
   then have carrier_subset_Units: "carrier G <= Units G"
     by (unfold Units_def) fast
-  show ?thesis proof qed (auto simp: r_one m_assoc carrier_subset_Units)
+  show ?thesis by default (auto simp: r_one m_assoc carrier_subset_Units)
 qed
 
 lemma (in monoid) group_l_invI:
@@ -694,7 +694,7 @@
   assumes m_comm: "!!x y. [| x \<in> carrier G; y \<in> carrier G |] ==>
       x \<otimes> y = y \<otimes> x"
   shows "comm_group G"
-  proof qed (simp_all add: m_comm)
+  by default (simp_all add: m_comm)
 
 lemma comm_groupI:
   fixes G (structure)
@@ -722,7 +722,7 @@
 
 theorem (in group) subgroups_partial_order:
   "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
-  proof qed simp_all
+  by default simp_all
 
 lemma (in group) subgroup_self:
   "subgroup (carrier G) G"
diff -r d80fe56788a5 -r fe0365331566 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Fri Sep 02 17:58:32 2011 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Fri Sep 02 18:17:45 2011 +0200
@@ -62,7 +62,7 @@
     and "pow \<Z> x n = x^n"
 proof -
   -- "Specification"
-  show "monoid \<Z>" proof qed auto
+  show "monoid \<Z>" by default auto
   then interpret int: monoid \<Z> .
 
   -- "Carrier"
@@ -79,7 +79,7 @@
   where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
 proof -
   -- "Specification"
-  show "comm_monoid \<Z>" proof qed auto
+  show "comm_monoid \<Z>" by default auto
   then interpret int: comm_monoid \<Z> .
 
   -- "Operations"
@@ -105,7 +105,7 @@
     and int_finsum_eq: "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
 proof -
   -- "Specification"
-  show "abelian_monoid \<Z>" proof qed auto
+  show "abelian_monoid \<Z>" by default auto
   then interpret int: abelian_monoid \<Z> .
 
   -- "Carrier"
@@ -189,7 +189,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> |)"
-    proof qed simp_all
+    by default 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)"
@@ -226,7 +226,7 @@
 
 interpretation int (* [unfolded UNIV] *) :
   total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
-  proof qed clarsimp
+  by default clarsimp
 
 
 subsection {* Generated Ideals of @{text "\<Z>"} *}
diff -r d80fe56788a5 -r fe0365331566 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Fri Sep 02 17:58:32 2011 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Fri Sep 02 18:17:45 2011 +0200
@@ -921,7 +921,7 @@
 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"
-  proof qed (rule total)
+  by default (rule total)
 
 text {* Total orders are lattices. *}
 
@@ -985,7 +985,7 @@
     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "weak_complete_lattice L"
-  proof qed (auto intro: sup_exists inf_exists)
+  by default (auto intro: sup_exists inf_exists)
 
 definition
   top :: "_ => 'a" ("\<top>\<index>")
@@ -1133,14 +1133,14 @@
     "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
 
 sublocale upper_semilattice < weak: weak_upper_semilattice
-  proof qed (rule sup_of_two_exists)
+  by default (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})"
 
 sublocale lower_semilattice < weak: weak_lower_semilattice
-  proof qed (rule inf_of_two_exists)
+  by default (rule inf_of_two_exists)
 
 locale lattice = upper_semilattice + lower_semilattice
 
@@ -1191,19 +1191,19 @@
   assumes total_order_total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
 
 sublocale total_order < weak: weak_total_order
-  proof qed (rule total_order_total)
+  by default (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"
-  proof qed (rule total)
+  by default (rule total)
 
 text {* Total orders are lattices. *}
 
 sublocale total_order < weak: lattice
-  proof qed (auto intro: sup_of_two_exists inf_of_two_exists)
+  by default (auto intro: sup_of_two_exists inf_of_two_exists)
 
 
 text {* Complete lattices *}
@@ -1215,7 +1215,7 @@
     "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
 
 sublocale complete_lattice < weak: weak_complete_lattice
-  proof qed (auto intro: sup_exists inf_exists)
+  by default (auto intro: sup_exists inf_exists)
 
 text {* Introduction rule: the usual definition of complete lattice *}
 
@@ -1225,7 +1225,7 @@
     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   shows "complete_lattice L"
-  proof qed (auto intro: sup_exists inf_exists)
+  by default (auto intro: sup_exists inf_exists)
 
 theorem (in partial_order) complete_lattice_criterion1:
   assumes top_exists: "EX g. greatest L g (carrier L)"
diff -r d80fe56788a5 -r fe0365331566 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Fri Sep 02 17:58:32 2011 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Fri Sep 02 18:17:45 2011 +0200
@@ -17,7 +17,7 @@
     and hom_one [simp] = ring_hom_one [OF homh]
 
 sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
-  proof qed (rule homh)
+  by default (rule homh)
 
 sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
 apply (rule abelian_group_homI)
diff -r d80fe56788a5 -r fe0365331566 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Sep 02 17:58:32 2011 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Sep 02 18:17:45 2011 +0200
@@ -1764,7 +1764,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 proof qed simp
+  interpret UP_pre_univ_prop R R id P by default 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"