# HG changeset patch
# User wenzelm
# Date 1204748643 -3600
# Node ID 04817a8802f296202bdb1eb4243f391341d2016f
# Parent  865bca530d4ca4192c6fddceef33d40a5081f8ce
explicit referencing of background facts;

diff -r 865bca530d4c -r 04817a8802f2 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Wed Mar 05 14:34:39 2008 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Wed Mar 05 21:24:03 2008 +0100
@@ -168,7 +168,7 @@
 
 ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
 
-lemma (in ID) th_y: "d == (a = b)" by fact
+lemma (in ID) th_y: "d == (a = b)" by (rule d_def)
 
 thm i2.th_y thm i3.th_y
 
diff -r 865bca530d4c -r 04817a8802f2 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Mar 05 14:34:39 2008 +0100
+++ b/src/HOL/Algebra/Group.thy	Wed Mar 05 21:24:03 2008 +0100
@@ -195,7 +195,7 @@
   assumes Units: "carrier G <= Units G"
 
 
-lemma (in group) is_group: "group G" by fact
+lemma (in group) is_group: "group G" by (rule group_axioms)
 
 theorem groupI:
   fixes G (structure)
@@ -383,7 +383,7 @@
     and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
 
 lemma (in subgroup) is_subgroup:
-  "subgroup H G" by fact
+  "subgroup H G" by (rule subgroup_axioms)
 
 declare (in subgroup) group.intro [intro]
 
@@ -694,7 +694,7 @@
 
 lemma (in group) subgroup_imp_group:
   "subgroup H G ==> group (G(| carrier := H |))"
-  by (erule subgroup.subgroup_is_group) (rule `group G`)
+  by (erule subgroup.subgroup_is_group) (rule group_axioms)
 
 lemma (in group) is_monoid [intro, simp]:
   "monoid G"
diff -r 865bca530d4c -r 04817a8802f2 src/HOL/Groebner_Basis.thy
--- a/src/HOL/Groebner_Basis.thy	Wed Mar 05 14:34:39 2008 +0100
+++ b/src/HOL/Groebner_Basis.thy	Wed Mar 05 21:24:03 2008 +0100
@@ -162,7 +162,7 @@
 lemma "axioms" [normalizer
     semiring ops: semiring_ops
     semiring rules: semiring_rules]:
-  "gb_semiring add mul pwr r0 r1" by fact
+  "gb_semiring add mul pwr r0 r1" by (rule gb_semiring_axioms)
 
 end
 
@@ -237,7 +237,7 @@
   semiring rules: semiring_rules
   ring ops: ring_ops
   ring rules: ring_rules]:
-  "gb_ring add mul pwr r0 r1 sub neg" by fact
+  "gb_ring add mul pwr r0 r1 sub neg" by (rule gb_ring_axioms)
 
 end
 
@@ -268,7 +268,7 @@
   semiring rules: semiring_rules
   ring ops: ring_ops
   ring rules: ring_rules]:
-  "gb_field add mul pwr r0 r1 sub neg divide inverse" by fact
+  "gb_field add mul pwr r0 r1 sub neg divide inverse" by (rule gb_field_axioms)
 
 end
 
@@ -313,7 +313,7 @@
   semiring ops: semiring_ops
   semiring rules: semiring_rules
   idom rules: noteq_reduce add_scale_eq_noteq]:
-  "semiringb add mul pwr r0 r1" by fact
+  "semiringb add mul pwr r0 r1" by (rule semiringb_axioms)
 
 end
 
@@ -330,7 +330,7 @@
   ring rules: ring_rules
   idom rules: noteq_reduce add_scale_eq_noteq
   ideal rules: subr0_iff add_r0_iff]:
-  "ringb add mul pwr r0 r1 sub neg" by fact
+  "ringb add mul pwr r0 r1 sub neg" by (rule ringb_axioms)
 
 end
 
diff -r 865bca530d4c -r 04817a8802f2 src/HOL/Library/Dense_Linear_Order.thy
--- a/src/HOL/Library/Dense_Linear_Order.thy	Wed Mar 05 14:34:39 2008 +0100
+++ b/src/HOL/Library/Dense_Linear_Order.thy	Wed Mar 05 21:24:03 2008 +0100
@@ -264,7 +264,7 @@
 lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq 
   le_less neq_iff linear less_not_permute
 
-lemma axiom: "dense_linear_order (op \<le>) (op <)" by fact
+lemma axiom: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms)
 lemma atoms:
   includes meta_term_syntax
   shows "TERM (less :: 'a \<Rightarrow> _)"
@@ -500,7 +500,8 @@
 lemmas npi_thms = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
 lemmas lin_dense_thms = lin_dense_conj lin_dense_disj lin_dense_eq lin_dense_neq lin_dense_lt lin_dense_le lin_dense_gt lin_dense_ge lin_dense_P
 
-lemma ferrack_axiom: "constr_dense_linear_order less_eq less between" by fact
+lemma ferrack_axiom: "constr_dense_linear_order less_eq less between"
+  by (rule constr_dense_linear_order_axioms)
 lemma atoms:
   includes meta_term_syntax
   shows "TERM (less :: 'a \<Rightarrow> _)"
diff -r 865bca530d4c -r 04817a8802f2 src/HOL/Real/HahnBanach/Subspace.thy
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed Mar 05 14:34:39 2008 +0100
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Wed Mar 05 21:24:03 2008 +0100
@@ -204,7 +204,7 @@
 proof -
   from `x \<in> V` have "subspace (lin x) V"
     by (rule lin_subspace)
-  from this and `vectorspace V` show ?thesis
+  from this and vectorspace_axioms show ?thesis
     by (rule subspace.vectorspace)
 qed
 
diff -r 865bca530d4c -r 04817a8802f2 src/ZF/ex/Group.thy
--- a/src/ZF/ex/Group.thy	Wed Mar 05 14:34:39 2008 +0100
+++ b/src/ZF/ex/Group.thy	Wed Mar 05 21:24:03 2008 +0100
@@ -92,7 +92,7 @@
   assumes inv_ex:
      "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
 
-lemma (in group) is_group [simp]: "group(G)" by fact
+lemma (in group) is_group [simp]: "group(G)" by (rule group_axioms)
 
 theorem groupI:
   includes struct G
@@ -1003,7 +1003,7 @@
   shows "H \<in> rcosets H"
 proof -
   have "H #> \<one> = H"
-    using _ `subgroup(H, G)` by (rule coset_join2) simp_all
+    using _ subgroup_axioms by (rule coset_join2) simp_all
   then show ?thesis
     by (auto simp add: RCOSETS_def intro: sym)
 qed