isabelle: src/HOL/Algebra/ROOT.ML@fc8419fd4735 (annotated)

35849 b5522b51cb1e standard headers; wenzelm parents: 32480 diff changeset	1	(* Author: Clemens Ballarin, started 24 September 1999
b5522b51cb1e standard headers; wenzelm parents: 32480 diff changeset	2
b5522b51cb1e standard headers; wenzelm parents: 32480 diff changeset	3	The Isabelle Algebraic Library.
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	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 6c19da8e661a some reorganization of number theory haftmann parents: 27713 diff changeset	7	no_document use_thys ["FuncSet", "~~/src/HOL/Old_Number_Theory/Primes", "Binomial", "Permutation"];
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20318 diff changeset	8
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	9
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	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 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	12	use_thys [
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	13	(* Groups *)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	14	"FiniteProduct", (* Product operator for commutative groups *)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	15	"Sylow", (* Sylow's theorem *)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	16	"Bij", (* Automorphism Groups *)
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	17
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	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 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	22	];
20318 0e0ea63fe768 Restructured algebra library, added ideals and quotient rings. ballarin parents: 14751 diff changeset	23
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	24
35849 b5522b51cb1e standard headers; wenzelm parents: 32480 diff changeset	25	(* Old development, based on axiomatic type classes *)
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	26
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	27	no_document use_thys [
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	28	"abstract/Abstract", (The ring theory)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	29	"poly/Polynomial" (The full theory)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	30	];

author	haftmann
	Mon, 20 Dec 2010 08:55:36 +0100
changeset 41299	fc8419fd4735
parent 35849	b5522b51cb1e
child 41413	64cd30d6b0b8
permissions	-rw-r--r--