src/HOL/Algebra/ROOT.ML
author wenzelm
Mon Mar 16 18:24:30 2009 +0100 (2009-03-16)
changeset 30549 d2d7874648bd
parent 27713 95b36bfe7fc4
child 32480 6c19da8e661a
permissions -rw-r--r--
simplified method setup;
     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", "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 ];