--- 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
--- 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"
--- 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
--- 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> _)"
--- 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
--- 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