author wenzelm Wed Mar 05 21:42:21 2008 +0100 (2008-03-05) changeset 26203 9625f3579b48 parent 26202 51f8a696cd8d child 26204 da9778392d8c
explicit referencing of background facts;
 src/HOL/Algebra/AbelCoset.thy file | annotate | diff | revisions src/HOL/Algebra/Coset.thy file | annotate | diff | revisions src/HOL/Algebra/Ideal.thy file | annotate | diff | revisions
```     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.7 -by fact
1.9
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
```