src/HOL/Algebra/ROOT.ML
author ballarin
Thu Aug 03 14:57:26 2006 +0200 (2006-08-03)
changeset 20318 0e0ea63fe768
parent 14751 0d7850e27fed
child 21256 47195501ecf7
permissions -rw-r--r--
Restructured algebra library, added ideals and quotient rings.
paulson@7998
     1
(*
ballarin@13936
     2
    The Isabelle Algebraic Library
paulson@7998
     3
    $Id$
paulson@7998
     4
    Author: Clemens Ballarin, started 24 September 1999
paulson@7998
     5
*)
paulson@7998
     6
ballarin@13949
     7
(*** New development, based on explicit structures ***)
ballarin@13949
     8
ballarin@13949
     9
(* Preliminaries from set and number theory *)
ballarin@13936
    10
ballarin@13940
    11
no_document use_thy "FuncSet";
ballarin@13949
    12
no_document use_thy "Primes";
ballarin@13949
    13
ballarin@13949
    14
(* Groups *)
ballarin@13949
    15
ballarin@13949
    16
use_thy "FiniteProduct";	(* Product operator for commutative groups *)
ballarin@13949
    17
use_thy "Sylow";		(* Sylow's theorem *)
paulson@13943
    18
use_thy "Bij";			(* Automorphism Groups *)
ballarin@13949
    19
ballarin@13949
    20
(* Rings *)
ballarin@13949
    21
ballarin@13940
    22
use_thy "UnivPoly";		(* Rings and polynomials *)
ballarin@20318
    23
use_thy "IntRing";		(* Ideals and residue classes *)
ballarin@20318
    24
ballarin@13936
    25
ballarin@13949
    26
(*** Old development, based on axiomatic type classes.
ballarin@13949
    27
     Will be withdrawn in future. ***)
ballarin@13936
    28
ballarin@13949
    29
with_path "abstract" (no_document time_use_thy) "Abstract";   (*The ring theory*)
ballarin@13949
    30
with_path "poly"     (no_document time_use_thy) "Polynomial"; (*The full theory*)