author | krauss |
Mon, 13 Nov 2006 21:52:14 +0100 | |
changeset 21346 | c8aa120fa05d |
parent 21256 | 47195501ecf7 |
child 24153 | 1a4607b7ad24 |
permissions | -rw-r--r-- |
7998 | 1 |
(* |
13936 | 2 |
The Isabelle Algebraic Library |
7998 | 3 |
$Id$ |
4 |
Author: Clemens Ballarin, started 24 September 1999 |
|
5 |
*) |
|
6 |
||
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
7 |
(*** New development, based on explicit structures ***) |
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
8 |
|
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
9 |
(* Preliminaries from set and number theory *) |
13936 | 10 |
|
13940 | 11 |
no_document use_thy "FuncSet"; |
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
12 |
no_document use_thy "Primes"; |
21256 | 13 |
no_document use_thy "Binomial"; |
14 |
||
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
15 |
|
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
16 |
(* Groups *) |
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
17 |
|
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
18 |
use_thy "FiniteProduct"; (* Product operator for commutative groups *) |
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
19 |
use_thy "Sylow"; (* Sylow's theorem *) |
13943 | 20 |
use_thy "Bij"; (* Automorphism Groups *) |
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
21 |
|
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
22 |
(* Rings *) |
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
23 |
|
13940 | 24 |
use_thy "UnivPoly"; (* Rings and polynomials *) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
14751
diff
changeset
|
25 |
use_thy "IntRing"; (* Ideals and residue classes *) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
14751
diff
changeset
|
26 |
|
13936 | 27 |
|
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
28 |
(*** Old development, based on axiomatic type classes. |
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
29 |
Will be withdrawn in future. ***) |
13936 | 30 |
|
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
31 |
with_path "abstract" (no_document time_use_thy) "Abstract"; (*The ring theory*) |
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
32 |
with_path "poly" (no_document time_use_thy) "Polynomial"; (*The full theory*) |