src/HOL/Algebra/ROOT.ML
changeset 13936 d3671b878828
parent 13870 cf947d1ec5ff
child 13940 c67798653056
     1.1 --- a/src/HOL/Algebra/ROOT.ML	Tue Apr 29 12:36:49 2003 +0200
     1.2 +++ b/src/HOL/Algebra/ROOT.ML	Wed Apr 30 10:01:35 2003 +0200
     1.3 @@ -1,9 +1,16 @@
     1.4  (*
     1.5 -    Polynomials
     1.6 +    The Isabelle Algebraic Library
     1.7      $Id$
     1.8      Author: Clemens Ballarin, started 24 September 1999
     1.9  *)
    1.10  
    1.11 +(* New development, based on explicit structures *)
    1.12 +
    1.13 +use_thy "Sylow";		(* Groups *)
    1.14 +(* use_thy "UnivPoly"; *)	(* Rings and polynomials *)
    1.15 +
    1.16 +(* Old development, based on axiomatic type classes.
    1.17 +   Will be withdrawn in future. *)
    1.18 +
    1.19  with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
    1.20  with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)
    1.21 -use_thy "Sylow";