src/HOL/Algebra/ROOT.ML
author ballarin
Wed Jul 30 19:03:33 2008 +0200 (2008-07-30)
changeset 27713 95b36bfe7fc4
parent 24153 1a4607b7ad24
child 32480 6c19da8e661a
permissions -rw-r--r--
New locales for orders and lattices where the equivalence relation is not restricted to equality.
     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 ];