summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Algebra/ROOT.ML

changeset 13949 | 0ce528cd6f19 |

parent 13943 | 83d842ccd4aa |

child 14551 | 2cb6ff394bfb |

1.1 --- a/src/HOL/Algebra/ROOT.ML Fri May 02 16:43:36 2003 +0200 1.2 +++ b/src/HOL/Algebra/ROOT.ML Fri May 02 20:02:50 2003 +0200 1.3 @@ -4,15 +4,25 @@ 1.4 Author: Clemens Ballarin, started 24 September 1999 1.5 *) 1.6 1.7 -(* New development, based on explicit structures *) 1.8 +(*** New development, based on explicit structures ***) 1.9 + 1.10 +(* Preliminaries from set and number theory *) 1.11 1.12 no_document use_thy "FuncSet"; 1.13 -use_thy "Sylow"; (* Groups *) 1.14 +no_document use_thy "Primes"; 1.15 + 1.16 +(* Groups *) 1.17 + 1.18 +use_thy "FiniteProduct"; (* Product operator for commutative groups *) 1.19 +use_thy "Sylow"; (* Sylow's theorem *) 1.20 use_thy "Bij"; (* Automorphism Groups *) 1.21 + 1.22 +(* Rings *) 1.23 + 1.24 use_thy "UnivPoly"; (* Rings and polynomials *) 1.25 1.26 -(* Old development, based on axiomatic type classes. 1.27 - Will be withdrawn in future. *) 1.28 +(*** Old development, based on axiomatic type classes. 1.29 + Will be withdrawn in future. ***) 1.30 1.31 -with_path "abstract" time_use_thy "Abstract"; (*The ring theory*) 1.32 -with_path "poly" time_use_thy "Polynomial"; (*The full theory*) 1.33 +with_path "abstract" (no_document time_use_thy) "Abstract"; (*The ring theory*) 1.34 +with_path "poly" (no_document time_use_thy) "Polynomial"; (*The full theory*)