isabelle: src/HOL/Algebra/ROOT.ML@480746f1012c (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 *)
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 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20318 diff changeset	13
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	14
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	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 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	17	use_thys [
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	18	(* Groups *)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	19	"FiniteProduct", (* Product operator for commutative groups *)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	20	"Sylow", (* Sylow's theorem *)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	21	"Bij", (* Automorphism Groups *)
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	22
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	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 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	27	];
20318 0e0ea63fe768 Restructured algebra library, added ideals and quotient rings. ballarin parents: 14751 diff changeset	28
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	29
35849 b5522b51cb1e standard headers; wenzelm parents: 32480 diff changeset	30	(* Old development, based on axiomatic type classes *)
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	31
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	32	no_document use_thys [
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	33	"abstract/Abstract", (The ring theory)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	34	"poly/Polynomial" (The full theory)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	35	];

author	blanchet
	Fri, 20 Jul 2012 22:19:46 +0200
changeset 48391	480746f1012c
parent 41413	64cd30d6b0b8
permissions	-rw-r--r--