# HG changeset patch
# User wenzelm
# Date 1204749741 -3600
# Node ID 9625f3579b4851e9c5f442cc22e6f61c7c9548ca
# Parent  51f8a696cd8da298430ef2bee3d5546572003e3a
explicit referencing of background facts;

diff -r 51f8a696cd8d -r 9625f3579b48 src/HOL/Algebra/AbelCoset.thy
--- 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>"
diff -r 51f8a696cd8d -r 9625f3579b48 src/HOL/Algebra/Coset.thy
--- 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)
diff -r 51f8a696cd8d -r 9625f3579b48 src/HOL/Algebra/Ideal.thy
--- 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