src/HOL/Algebra/ROOT.ML
author paulson
Fri, 05 Nov 1999 11:14:26 +0100
changeset 7998 3d0c34795831
child 8010 69032a618aa9
permissions -rw-r--r--
Algebra and Polynomial theories, by Clemens Ballarin
     1 (*
     2     Polynomials
     3     $Id$
     4     Author: Clemens Ballarin, started 24 September 1999
     5 *)
     6 
     7 add_path "abstract";
     8 add_path "poly";
     9 
    10 use_thy "Abstract";	(*The ring theory*)
    11 use_thy "Polynomial";	(*The full theory*)