author | bulwahn |
Fri, 03 Dec 2010 08:40:47 +0100 | |
changeset 40905 | 647142607448 |
parent 35849 | b5522b51cb1e |
child 41413 | 64cd30d6b0b8 |
permissions | -rw-r--r-- |
35849 | 1 |
(* Author: Clemens Ballarin, started 24 September 1999 |
2 |
||
3 |
The Isabelle Algebraic Library. |
|
7998 | 4 |
*) |
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 | 7 |
no_document use_thys ["FuncSet", "~~/src/HOL/Old_Number_Theory/Primes", "Binomial", "Permutation"]; |
21256 | 8 |
|
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
9 |
|
24153 | 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 | 12 |
use_thys [ |
13 |
(* Groups *) |
|
14 |
"FiniteProduct", (* Product operator for commutative groups *) |
|
15 |
"Sylow", (* Sylow's theorem *) |
|
16 |
"Bij", (* Automorphism Groups *) |
|
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
17 |
|
24153 | 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 | 22 |
]; |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
14751
diff
changeset
|
23 |
|
13936 | 24 |
|
35849 | 25 |
(*** Old development, based on axiomatic type classes ***) |
13936 | 26 |
|
24153 | 27 |
no_document use_thys [ |
28 |
"abstract/Abstract", (*The ring theory*) |
|
29 |
"poly/Polynomial" (*The full theory*) |
|
30 |
]; |