src/HOL/Algebra/ROOT.ML
author wenzelm
Sun Mar 21 15:57:40 2010 +0100 (2010-03-21)
changeset 35847 19f1f7066917
parent 32480 6c19da8e661a
child 35849 b5522b51cb1e
permissions -rw-r--r--
eliminated old constdefs;
     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", "~~/src/HOL/Old_Number_Theory/Primes", "Binomial", "Permutation"];
     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   "Divisibility",       (* Rings *)
    21   "IntRing",            (* Ideals and residue classes *)
    22   "UnivPoly"            (* Polynomials *)
    23 ];
    24 
    25 
    26 (*** Old development, based on axiomatic type classes.
    27      Will be withdrawn in future. ***)
    28 
    29 no_document use_thys [
    30   "abstract/Abstract",  (*The ring theory*)
    31   "poly/Polynomial"     (*The full theory*)
    32 ];