src/HOL/Algebra/ROOT.ML
author haftmann
Tue Sep 01 16:00:57 2009 +0200 (2009-09-01)
changeset 32480 6c19da8e661a
parent 27713 95b36bfe7fc4
child 35849 b5522b51cb1e
permissions -rw-r--r--
some reorganization of number theory
     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 ];