--- 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:
--- 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)"
--- 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"
--- 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>"} *}
--- 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)"
--- 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)
--- 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"