src/HOL/Algebra/ROOT.ML
author nipkow
Fri, 13 Nov 2009 14:14:04 +0100
changeset 33657 a4179bf442d1
parent 32480 6c19da8e661a
child 35849 b5522b51cb1e
permissions -rw-r--r--
renamed lemmas "anti_sym" -> "antisym"
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7998
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     1
(*
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13870
diff changeset
     2
    The Isabelle Algebraic Library
7998
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     3
    $Id$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     4
    Author: Clemens Ballarin, started 24 September 1999
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     5
*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     6
13949
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents: 13943
diff changeset
     7
(* Preliminaries from set and number theory *)
32480
6c19da8e661a some reorganization of number theory
haftmann
parents: 27713
diff changeset
     8
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
     9
13949
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents: 13943
diff changeset
    10
24153
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    11
(*** New development, based on explicit structures ***)
13949
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents: 13943
diff changeset
    12
24153
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    13
use_thys [
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    14
  (* Groups *)
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    15
  "FiniteProduct",      (* Product operator for commutative groups *)
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    16
  "Sylow",              (* Sylow's theorem *)
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    17
  "Bij",                (* Automorphism Groups *)
13949
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents: 13943
diff changeset
    18
24153
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    19
  (* Rings *)
27713
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 24153
diff changeset
    20
  "Divisibility",       (* Rings *)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents: 24153
diff changeset
    21
  "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
    22
  "UnivPoly"            (* Polynomials *)
24153
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    23
];
20318
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings.
ballarin
parents: 14751
diff changeset
    24
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13870
diff changeset
    25
13949
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents: 13943
diff changeset
    26
(*** Old development, based on axiomatic type classes.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents: 13943
diff changeset
    27
     Will be withdrawn in future. ***)
13936
d3671b878828 Greatly extended CRing. Added Module.
ballarin
parents: 13870
diff changeset
    28
24153
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    29
no_document use_thys [
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    30
  "abstract/Abstract",  (*The ring theory*)
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    31
  "poly/Polynomial"     (*The full theory*)
1a4607b7ad24 simultaneous use_thys;
wenzelm
parents: 21256
diff changeset
    32
];