src/HOL/Algebra/ROOT.ML
author ballarin
Wed Apr 30 18:32:06 2003 +0200 (2003-04-30)
changeset 13940 c67798653056
parent 13936 d3671b878828
child 13943 83d842ccd4aa
permissions -rw-r--r--
HOL-Algebra: New polynomial development added.
     1 (*
     2     The Isabelle Algebraic Library
     3     $Id$
     4     Author: Clemens Ballarin, started 24 September 1999
     5 *)
     6 
     7 (* New development, based on explicit structures *)
     8 
     9 no_document use_thy "FuncSet";
    10 use_thy "Sylow";		(* Groups *)
    11 use_thy "UnivPoly";		(* Rings and polynomials *)
    12 
    13 (* Old development, based on axiomatic type classes.
    14    Will be withdrawn in future. *)
    15 
    16 with_path "abstract" time_use_thy "Abstract";        (*The ring theory*)
    17 with_path "poly"     time_use_thy "Polynomial";      (*The full theory*)