author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 32480  6c19da8e661a 
child 35849  b5522b51cb1e 
permissions  rwrr 
7998  1 
(* 
13936  2 
The Isabelle Algebraic Library 
7998  3 
$Id$ 
4 
Author: Clemens Ballarin, started 24 September 1999 

5 
*) 

6 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset

7 
(* Preliminaries from set and number theory *) 
32480  8 
no_document use_thys ["FuncSet", "~~/src/HOL/Old_Number_Theory/Primes", "Binomial", "Permutation"]; 
21256  9 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset

10 

24153  11 
(*** New development, based on explicit structures ***) 
13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset

12 

24153  13 
use_thys [ 
14 
(* Groups *) 

15 
"FiniteProduct", (* Product operator for commutative groups *) 

16 
"Sylow", (* Sylow's theorem *) 

17 
"Bij", (* Automorphism Groups *) 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset

18 

24153  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  23 
]; 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
14751
diff
changeset

24 

13936  25 

13949
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset

26 
(*** Old development, based on axiomatic type classes. 
0ce528cd6f19
HOLAlgebra complete for release Isabelle2003 (modulo section headers).
ballarin
parents:
13943
diff
changeset

27 
Will be withdrawn in future. ***) 
13936  28 

24153  29 
no_document use_thys [ 
30 
"abstract/Abstract", (*The ring theory*) 

31 
"poly/Polynomial" (*The full theory*) 

32 
]; 