src/HOL/Algebra/ROOT.ML
author ballarin
Fri May 14 19:29:22 2004 +0200 (2004-05-14)
changeset 14751 0d7850e27fed
parent 14551 2cb6ff394bfb
child 20318 0e0ea63fe768
permissions -rw-r--r--
Change of theory hierarchy: Group is now based in Lattice.
     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 (* Preliminaries from set and number theory *)
    10 
    11 no_document use_thy "FuncSet";
    12 no_document use_thy "Primes";
    13 
    14 (* Groups *)
    15 
    16 use_thy "FiniteProduct";	(* Product operator for commutative groups *)
    17 use_thy "Sylow";		(* Sylow's theorem *)
    18 use_thy "Bij";			(* Automorphism Groups *)
    19 
    20 (* Rings *)
    21 
    22 use_thy "UnivPoly";		(* Rings and polynomials *)
    23 
    24 (*** Old development, based on axiomatic type classes.
    25      Will be withdrawn in future. ***)
    26 
    27 with_path "abstract" (no_document time_use_thy) "Abstract";   (*The ring theory*)
    28 with_path "poly"     (no_document time_use_thy) "Polynomial"; (*The full theory*)