(* Author: Clemens Ballarin, started 24 September 1999
The Isabelle Algebraic Library.
*)
(* Preliminaries from set and number theory *)
no_document use_thys [
"~~/src/HOL/Library/FuncSet",
"~~/src/HOL/Old_Number_Theory/Primes",
"~~/src/HOL/Library/Binomial",
"~~/src/HOL/Library/Permutation"
];
(*** New development, based on explicit structures ***)
use_thys [
(* Groups *)
"FiniteProduct", (* Product operator for commutative groups *)
"Sylow", (* Sylow's theorem *)
"Bij", (* Automorphism Groups *)
(* Rings *)
"Divisibility", (* Rings *)
"IntRing", (* Ideals and residue classes *)
"UnivPoly" (* Polynomials *)
];
(*** Old development, based on axiomatic type classes ***)
no_document use_thys [
"abstract/Abstract", (*The ring theory*)
"poly/Polynomial" (*The full theory*)
];