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*)