src/HOL/Algebra/ROOT.ML
author wenzelm
Fri Aug 03 22:50:40 2007 +0200 (2007-08-03)
changeset 24153 1a4607b7ad24
parent 21256 47195501ecf7
child 27713 95b36bfe7fc4
permissions -rw-r--r--
simultaneous use_thys;
     1 (*
     2     The Isabelle Algebraic Library
     3     $Id$
     4     Author: Clemens Ballarin, started 24 September 1999
     5 *)
     6 
     7 (* Preliminaries from set and number theory *)
     8 no_document use_thys ["FuncSet", "Primes", "Binomial"];
     9 
    10 
    11 (*** New development, based on explicit structures ***)
    12 
    13 use_thys [
    14   (* Groups *)
    15   "FiniteProduct",      (* Product operator for commutative groups *)
    16   "Sylow",              (* Sylow's theorem *)
    17   "Bij",                (* Automorphism Groups *)
    18 
    19   (* Rings *)
    20   "UnivPoly",           (* Rings and polynomials *)
    21   "IntRing"             (* Ideals and residue classes *)
    22 ];
    23 
    24 
    25 (*** Old development, based on axiomatic type classes.
    26      Will be withdrawn in future. ***)
    27 
    28 no_document use_thys [
    29   "abstract/Abstract",  (*The ring theory*)
    30   "poly/Polynomial"     (*The full theory*)
    31 ];