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
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";
wenzelm@21256
    13
no_document use_thy "Binomial";
wenzelm@21256
    14
ballarin@13949
    15
ballarin@13949
    16
(* Groups *)
ballarin@13949
    17
ballarin@13949
    18
use_thy "FiniteProduct";	(* Product operator for commutative groups *)
ballarin@13949
    19
use_thy "Sylow";		(* Sylow's theorem *)
paulson@13943
    20
use_thy "Bij";			(* Automorphism Groups *)
ballarin@13949
    21
ballarin@13949
    22
(* Rings *)
ballarin@13949
    23
ballarin@13940
    24
use_thy "UnivPoly";		(* Rings and polynomials *)
ballarin@20318
    25
use_thy "IntRing";		(* Ideals and residue classes *)
ballarin@20318
    26
ballarin@13936
    27
ballarin@13949
    28
(*** Old development, based on axiomatic type classes.
ballarin@13949
    29
     Will be withdrawn in future. ***)
ballarin@13936
    30
ballarin@13949
    31
with_path "abstract" (no_document time_use_thy) "Abstract";   (*The ring theory*)
ballarin@13949
    32
with_path "poly"     (no_document time_use_thy) "Polynomial"; (*The full theory*)