--- a/src/HOL/Algebra/AbelCoset.thy Wed Mar 05 21:33:59 2008 +0100
+++ b/src/HOL/Algebra/AbelCoset.thy Wed Mar 05 21:42:21 2008 +0100
@@ -185,7 +185,7 @@
lemma (in additive_subgroup) is_additive_subgroup:
shows "additive_subgroup H G"
-by fact
+by (rule additive_subgroup_axioms)
lemma additive_subgroupI:
includes struct G
@@ -225,7 +225,7 @@
lemma (in abelian_subgroup) is_abelian_subgroup:
shows "abelian_subgroup H G"
-by fact
+by (rule abelian_subgroup_axioms)
lemma abelian_subgroupI:
assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
--- a/src/HOL/Algebra/Coset.thy Wed Mar 05 21:33:59 2008 +0100
+++ b/src/HOL/Algebra/Coset.thy Wed Mar 05 21:42:21 2008 +0100
@@ -826,7 +826,7 @@
includes group G
shows "H \<in> rcosets H"
proof -
- from _ `subgroup H G` have "H #> \<one> = H"
+ from _ subgroup_axioms have "H #> \<one> = H"
by (rule coset_join2) auto
then show ?thesis
by (auto simp add: RCOSETS_def)
--- a/src/HOL/Algebra/Ideal.thy Wed Mar 05 21:33:59 2008 +0100
+++ b/src/HOL/Algebra/Ideal.thy Wed Mar 05 21:42:21 2008 +0100
@@ -25,7 +25,7 @@
lemma (in ideal) is_ideal:
"ideal I R"
-by fact
+by (rule ideal_axioms)
lemma idealI:
includes ring
@@ -55,7 +55,7 @@
lemma (in principalideal) is_principalideal:
shows "principalideal I R"
-by fact
+by (rule principalideal_axioms)
lemma principalidealI:
includes ideal
@@ -72,7 +72,7 @@
lemma (in maximalideal) is_maximalideal:
shows "maximalideal I R"
-by fact
+by (rule maximalideal_axioms)
lemma maximalidealI:
includes ideal
@@ -91,7 +91,7 @@
lemma (in primeideal) is_primeideal:
shows "primeideal I R"
-by fact
+by (rule primeideal_axioms)
lemma primeidealI:
includes ideal