src/HOL/Algebra/ROOT.ML
changeset 7998 3d0c34795831
child 8010 69032a618aa9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/ROOT.ML	Fri Nov 05 11:14:26 1999 +0100
     1.3 @@ -0,0 +1,11 @@
     1.4 +(*
     1.5 +    Polynomials
     1.6 +    $Id$
     1.7 +    Author: Clemens Ballarin, started 24 September 1999
     1.8 +*)
     1.9 +
    1.10 +add_path "abstract";
    1.11 +add_path "poly";
    1.12 +
    1.13 +use_thy "Abstract";	(*The ring theory*)
    1.14 +use_thy "Polynomial";	(*The full theory*)