src/HOL/Algebra/ROOT.ML
author haftmann
Fri Apr 20 11:21:42 2007 +0200 (2007-04-20)
changeset 22744 5cbe966d67a2
parent 21256 47195501ecf7
child 24153 1a4607b7ad24
permissions -rw-r--r--
Isar definitions are now added explicitly to code theorem table
     1 (*
     2     The Isabelle Algebraic Library
     3     $Id$
     4     Author: Clemens Ballarin, started 24 September 1999
     5 *)
     6 
     7 (*** New development, based on explicit structures ***)
     8 
     9 (* Preliminaries from set and number theory *)
    10 
    11 no_document use_thy "FuncSet";
    12 no_document use_thy "Primes";
    13 no_document use_thy "Binomial";
    14 
    15 
    16 (* Groups *)
    17 
    18 use_thy "FiniteProduct";	(* Product operator for commutative groups *)
    19 use_thy "Sylow";		(* Sylow's theorem *)
    20 use_thy "Bij";			(* Automorphism Groups *)
    21 
    22 (* Rings *)
    23 
    24 use_thy "UnivPoly";		(* Rings and polynomials *)
    25 use_thy "IntRing";		(* Ideals and residue classes *)
    26 
    27 
    28 (*** Old development, based on axiomatic type classes.
    29      Will be withdrawn in future. ***)
    30 
    31 with_path "abstract" (no_document time_use_thy) "Abstract";   (*The ring theory*)
    32 with_path "poly"     (no_document time_use_thy) "Polynomial"; (*The full theory*)