explicit referencing of background facts;
authorwenzelm
Wed Mar 05 21:24:03 2008 +0100 (2008-03-05)
changeset 2619904817a8802f2
parent 26198 865bca530d4c
child 26200 6bae051e8b7e
explicit referencing of background facts;
src/FOL/ex/LocaleTest.thy
src/HOL/Algebra/Group.thy
src/HOL/Groebner_Basis.thy
src/HOL/Library/Dense_Linear_Order.thy
src/HOL/Real/HahnBanach/Subspace.thy
src/ZF/ex/Group.thy
     1.1 --- a/src/FOL/ex/LocaleTest.thy	Wed Mar 05 14:34:39 2008 +0100
     1.2 +++ b/src/FOL/ex/LocaleTest.thy	Wed Mar 05 21:24:03 2008 +0100
     1.3 @@ -168,7 +168,7 @@
     1.4  
     1.5  ML {* check_thm "i2.th_x"; check_thm "i3.th_x" *}
     1.6  
     1.7 -lemma (in ID) th_y: "d == (a = b)" by fact
     1.8 +lemma (in ID) th_y: "d == (a = b)" by (rule d_def)
     1.9  
    1.10  thm i2.th_y thm i3.th_y
    1.11  
     2.1 --- a/src/HOL/Algebra/Group.thy	Wed Mar 05 14:34:39 2008 +0100
     2.2 +++ b/src/HOL/Algebra/Group.thy	Wed Mar 05 21:24:03 2008 +0100
     2.3 @@ -195,7 +195,7 @@
     2.4    assumes Units: "carrier G <= Units G"
     2.5  
     2.6  
     2.7 -lemma (in group) is_group: "group G" by fact
     2.8 +lemma (in group) is_group: "group G" by (rule group_axioms)
     2.9  
    2.10  theorem groupI:
    2.11    fixes G (structure)
    2.12 @@ -383,7 +383,7 @@
    2.13      and m_inv_closed [intro,simp]: "x \<in> H \<Longrightarrow> inv x \<in> H"
    2.14  
    2.15  lemma (in subgroup) is_subgroup:
    2.16 -  "subgroup H G" by fact
    2.17 +  "subgroup H G" by (rule subgroup_axioms)
    2.18  
    2.19  declare (in subgroup) group.intro [intro]
    2.20  
    2.21 @@ -694,7 +694,7 @@
    2.22  
    2.23  lemma (in group) subgroup_imp_group:
    2.24    "subgroup H G ==> group (G(| carrier := H |))"
    2.25 -  by (erule subgroup.subgroup_is_group) (rule `group G`)
    2.26 +  by (erule subgroup.subgroup_is_group) (rule group_axioms)
    2.27  
    2.28  lemma (in group) is_monoid [intro, simp]:
    2.29    "monoid G"
     3.1 --- a/src/HOL/Groebner_Basis.thy	Wed Mar 05 14:34:39 2008 +0100
     3.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Mar 05 21:24:03 2008 +0100
     3.3 @@ -162,7 +162,7 @@
     3.4  lemma "axioms" [normalizer
     3.5      semiring ops: semiring_ops
     3.6      semiring rules: semiring_rules]:
     3.7 -  "gb_semiring add mul pwr r0 r1" by fact
     3.8 +  "gb_semiring add mul pwr r0 r1" by (rule gb_semiring_axioms)
     3.9  
    3.10  end
    3.11  
    3.12 @@ -237,7 +237,7 @@
    3.13    semiring rules: semiring_rules
    3.14    ring ops: ring_ops
    3.15    ring rules: ring_rules]:
    3.16 -  "gb_ring add mul pwr r0 r1 sub neg" by fact
    3.17 +  "gb_ring add mul pwr r0 r1 sub neg" by (rule gb_ring_axioms)
    3.18  
    3.19  end
    3.20  
    3.21 @@ -268,7 +268,7 @@
    3.22    semiring rules: semiring_rules
    3.23    ring ops: ring_ops
    3.24    ring rules: ring_rules]:
    3.25 -  "gb_field add mul pwr r0 r1 sub neg divide inverse" by fact
    3.26 +  "gb_field add mul pwr r0 r1 sub neg divide inverse" by (rule gb_field_axioms)
    3.27  
    3.28  end
    3.29  
    3.30 @@ -313,7 +313,7 @@
    3.31    semiring ops: semiring_ops
    3.32    semiring rules: semiring_rules
    3.33    idom rules: noteq_reduce add_scale_eq_noteq]:
    3.34 -  "semiringb add mul pwr r0 r1" by fact
    3.35 +  "semiringb add mul pwr r0 r1" by (rule semiringb_axioms)
    3.36  
    3.37  end
    3.38  
    3.39 @@ -330,7 +330,7 @@
    3.40    ring rules: ring_rules
    3.41    idom rules: noteq_reduce add_scale_eq_noteq
    3.42    ideal rules: subr0_iff add_r0_iff]:
    3.43 -  "ringb add mul pwr r0 r1 sub neg" by fact
    3.44 +  "ringb add mul pwr r0 r1 sub neg" by (rule ringb_axioms)
    3.45  
    3.46  end
    3.47  
     4.1 --- a/src/HOL/Library/Dense_Linear_Order.thy	Wed Mar 05 14:34:39 2008 +0100
     4.2 +++ b/src/HOL/Library/Dense_Linear_Order.thy	Wed Mar 05 21:24:03 2008 +0100
     4.3 @@ -264,7 +264,7 @@
     4.4  lemmas dlo_simps = order_refl less_irrefl not_less not_le exists_neq 
     4.5    le_less neq_iff linear less_not_permute
     4.6  
     4.7 -lemma axiom: "dense_linear_order (op \<le>) (op <)" by fact
     4.8 +lemma axiom: "dense_linear_order (op \<le>) (op <)" by (rule dense_linear_order_axioms)
     4.9  lemma atoms:
    4.10    includes meta_term_syntax
    4.11    shows "TERM (less :: 'a \<Rightarrow> _)"
    4.12 @@ -500,7 +500,8 @@
    4.13  lemmas npi_thms = npi_conj npi_disj npi_eq npi_neq npi_lt npi_le npi_gt npi_ge npi_P
    4.14  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
    4.15  
    4.16 -lemma ferrack_axiom: "constr_dense_linear_order less_eq less between" by fact
    4.17 +lemma ferrack_axiom: "constr_dense_linear_order less_eq less between"
    4.18 +  by (rule constr_dense_linear_order_axioms)
    4.19  lemma atoms:
    4.20    includes meta_term_syntax
    4.21    shows "TERM (less :: 'a \<Rightarrow> _)"
     5.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Wed Mar 05 14:34:39 2008 +0100
     5.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Wed Mar 05 21:24:03 2008 +0100
     5.3 @@ -204,7 +204,7 @@
     5.4  proof -
     5.5    from `x \<in> V` have "subspace (lin x) V"
     5.6      by (rule lin_subspace)
     5.7 -  from this and `vectorspace V` show ?thesis
     5.8 +  from this and vectorspace_axioms show ?thesis
     5.9      by (rule subspace.vectorspace)
    5.10  qed
    5.11  
     6.1 --- a/src/ZF/ex/Group.thy	Wed Mar 05 14:34:39 2008 +0100
     6.2 +++ b/src/ZF/ex/Group.thy	Wed Mar 05 21:24:03 2008 +0100
     6.3 @@ -92,7 +92,7 @@
     6.4    assumes inv_ex:
     6.5       "\<And>x. x \<in> carrier(G) \<Longrightarrow> \<exists>y \<in> carrier(G). y \<cdot> x = \<one> & x \<cdot> y = \<one>"
     6.6  
     6.7 -lemma (in group) is_group [simp]: "group(G)" by fact
     6.8 +lemma (in group) is_group [simp]: "group(G)" by (rule group_axioms)
     6.9  
    6.10  theorem groupI:
    6.11    includes struct G
    6.12 @@ -1003,7 +1003,7 @@
    6.13    shows "H \<in> rcosets H"
    6.14  proof -
    6.15    have "H #> \<one> = H"
    6.16 -    using _ `subgroup(H, G)` by (rule coset_join2) simp_all
    6.17 +    using _ subgroup_axioms by (rule coset_join2) simp_all
    6.18    then show ?thesis
    6.19      by (auto simp add: RCOSETS_def intro: sym)
    6.20  qed