src/HOL/Algebra/ROOT.ML
author bulwahn
Fri, 03 Dec 2010 08:40:47 +0100
changeset 40905 647142607448
parent 35849 b5522b51cb1e
child 41413 64cd30d6b0b8
permissions -rw-r--r--
only handle TimeOut exception if used interactively
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35849
b5522b51cb1e standard headers;
wenzelm
parents: 32480
diff changeset
     1
(*  Author: Clemens Ballarin, started 24 September 1999
b5522b51cb1e standard headers;
wenzelm
parents: 32480
diff changeset
     2
b5522b51cb1e standard headers;
wenzelm
parents: 32480
diff changeset
     3
The Isabelle Algebraic Library.
7998
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     4
*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     5
13949
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents: 13943
diff changeset
     6
(* Preliminaries from set and number theory *)
32480
6c19da8e661a some reorganization of number theory
haftmann
parents: 27713
diff changeset
     7
no_document use_thys ["FuncSet", "~~/src/HOL/Old_Number_Theory/Primes", "Binomial", "Permutation"];
21256
47195501ecf7 moved theories Parity, GCD, Binomial to Library;
wenzelm
parents: 20318
diff changeset
     8
13949
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents: 13943
diff changeset
     9
24153
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    10
(*** New development, based on explicit structures ***)
13949
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents: 13943
diff changeset
    11
24153
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    12
use_thys [
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    13
  (* Groups *)
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    14
  "FiniteProduct",      (* Product operator for commutative groups *)
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    15
  "Sylow",              (* Sylow's theorem *)
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    16
  "Bij",                (* Automorphism Groups *)
13949
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents: 13943
diff changeset
    17
24153
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    18
  (* Rings *)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 24153
diff changeset
    19
  "Divisibility",       (* Rings *)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 24153
diff changeset
    20
  "IntRing",            (* Ideals and residue classes *)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 24153
diff changeset
    21
  "UnivPoly"            (* Polynomials *)
24153
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    22
];
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 14751
diff changeset
    23
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13870
diff changeset
    24
35849
b5522b51cb1e standard headers;
wenzelm
parents: 32480
diff changeset
    25
(*** Old development, based on axiomatic type classes ***)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13870
diff changeset
    26
24153
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    27
no_document use_thys [
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    28
  "abstract/Abstract",  (*The ring theory*)
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    29
  "poly/Polynomial"     (*The full theory*)
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    30
];