explicit referencing of background facts;
authorwenzelm
Wed Mar 05 21:42:21 2008 +0100 (2008-03-05)
changeset 262039625f3579b48
parent 26202 51f8a696cd8d
child 26204 da9778392d8c
explicit referencing of background facts;
src/HOL/Algebra/AbelCoset.thy
src/HOL/Algebra/Coset.thy
src/HOL/Algebra/Ideal.thy
     1.1 --- a/src/HOL/Algebra/AbelCoset.thy	Wed Mar 05 21:33:59 2008 +0100
     1.2 +++ b/src/HOL/Algebra/AbelCoset.thy	Wed Mar 05 21:42:21 2008 +0100
     1.3 @@ -185,7 +185,7 @@
     1.4  
     1.5  lemma (in additive_subgroup) is_additive_subgroup:
     1.6    shows "additive_subgroup H G"
     1.7 -by fact
     1.8 +by (rule additive_subgroup_axioms)
     1.9  
    1.10  lemma additive_subgroupI:
    1.11    includes struct G
    1.12 @@ -225,7 +225,7 @@
    1.13  
    1.14  lemma (in abelian_subgroup) is_abelian_subgroup:
    1.15    shows "abelian_subgroup H G"
    1.16 -by fact
    1.17 +by (rule abelian_subgroup_axioms)
    1.18  
    1.19  lemma abelian_subgroupI:
    1.20    assumes a_normal: "normal H \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
     2.1 --- a/src/HOL/Algebra/Coset.thy	Wed Mar 05 21:33:59 2008 +0100
     2.2 +++ b/src/HOL/Algebra/Coset.thy	Wed Mar 05 21:42:21 2008 +0100
     2.3 @@ -826,7 +826,7 @@
     2.4    includes group G
     2.5    shows "H \<in> rcosets H"
     2.6  proof -
     2.7 -  from _ `subgroup H G` have "H #> \<one> = H"
     2.8 +  from _ subgroup_axioms have "H #> \<one> = H"
     2.9      by (rule coset_join2) auto
    2.10    then show ?thesis
    2.11      by (auto simp add: RCOSETS_def)
     3.1 --- a/src/HOL/Algebra/Ideal.thy	Wed Mar 05 21:33:59 2008 +0100
     3.2 +++ b/src/HOL/Algebra/Ideal.thy	Wed Mar 05 21:42:21 2008 +0100
     3.3 @@ -25,7 +25,7 @@
     3.4  
     3.5  lemma (in ideal) is_ideal:
     3.6    "ideal I R"
     3.7 -by fact
     3.8 +by (rule ideal_axioms)
     3.9  
    3.10  lemma idealI:
    3.11    includes ring
    3.12 @@ -55,7 +55,7 @@
    3.13  
    3.14  lemma (in principalideal) is_principalideal:
    3.15    shows "principalideal I R"
    3.16 -by fact
    3.17 +by (rule principalideal_axioms)
    3.18  
    3.19  lemma principalidealI:
    3.20    includes ideal
    3.21 @@ -72,7 +72,7 @@
    3.22  
    3.23  lemma (in maximalideal) is_maximalideal:
    3.24   shows "maximalideal I R"
    3.25 -by fact
    3.26 +by (rule maximalideal_axioms)
    3.27  
    3.28  lemma maximalidealI:
    3.29    includes ideal
    3.30 @@ -91,7 +91,7 @@
    3.31  
    3.32  lemma (in primeideal) is_primeideal:
    3.33   shows "primeideal I R"
    3.34 -by fact
    3.35 +by (rule primeideal_axioms)
    3.36  
    3.37  lemma primeidealI:
    3.38    includes ideal