author | wenzelm |
Tue, 08 Feb 2011 16:11:52 +0100 | |
changeset 41715 | 22f8c2483bd2 |
parent 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 *) |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
35849
diff
changeset
|
7 |
no_document use_thys [ |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
35849
diff
changeset
|
8 |
"~~/src/HOL/Library/FuncSet", |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
35849
diff
changeset
|
9 |
"~~/src/HOL/Old_Number_Theory/Primes", |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
35849
diff
changeset
|
10 |
"~~/src/HOL/Library/Binomial", |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
35849
diff
changeset
|
11 |
"~~/src/HOL/Library/Permutation" |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
35849
diff
changeset
|
12 |
]; |
21256 | 13 |
|
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
14 |
|
24153 | 15 |
(*** New development, based on explicit structures ***) |
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
16 |
|
24153 | 17 |
use_thys [ |
18 |
(* Groups *) |
|
19 |
"FiniteProduct", (* Product operator for commutative groups *) |
|
20 |
"Sylow", (* Sylow's theorem *) |
|
21 |
"Bij", (* Automorphism Groups *) |
|
13949
0ce528cd6f19
HOL-Algebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset
|
22 |
|
24153 | 23 |
(* Rings *) |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
24153
diff
changeset
|
24 |
"Divisibility", (* Rings *) |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
24153
diff
changeset
|
25 |
"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
|
26 |
"UnivPoly" (* Polynomials *) |
24153 | 27 |
]; |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
14751
diff
changeset
|
28 |
|
13936 | 29 |
|
35849 | 30 |
(*** Old development, based on axiomatic type classes ***) |
13936 | 31 |
|
24153 | 32 |
no_document use_thys [ |
33 |
"abstract/Abstract", (*The ring theory*) |
|
34 |
"poly/Polynomial" (*The full theory*) |
|
35 |
]; |