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

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	(*
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	2	The Isabelle Algebraic Library
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3	$Id$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	Author: Clemens Ballarin, started 24 September 1999
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	5	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	6
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	7	(* New development, based on explicit structures *)
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	8
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	9	(* Preliminaries from set and number theory *)
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	10
13940 c67798653056 HOL-Algebra: New polynomial development added. ballarin parents: 13936 diff changeset	11	no_document use_thy "FuncSet";
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	12	no_document use_thy "Primes";
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20318 diff changeset	13	no_document use_thy "Binomial";
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20318 diff changeset	14
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	15
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	16	(* Groups *)
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	17
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	18	use_thy "FiniteProduct"; (* Product operator for commutative groups *)
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	19	use_thy "Sylow"; (* Sylow's theorem *)
13943 83d842ccd4aa moving Bij.thy from GroupTheory to Algebra paulson parents: 13940 diff changeset	20	use_thy "Bij"; (* Automorphism Groups *)
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	21
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	22	(* Rings *)
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	23
13940 c67798653056 HOL-Algebra: New polynomial development added. ballarin parents: 13936 diff changeset	24	use_thy "UnivPoly"; (* Rings and polynomials *)
20318 0e0ea63fe768 Restructured algebra library, added ideals and quotient rings. ballarin parents: 14751 diff changeset	25	use_thy "IntRing"; (* Ideals and residue classes *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings. ballarin parents: 14751 diff changeset	26
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	27
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	28	(*** Old development, based on axiomatic type classes.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	29	Will be withdrawn in future. ***)
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	30
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	31	with_path "abstract" (no_document time_use_thy) "Abstract"; (The ring theory)
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	32	with_path "poly" (no_document time_use_thy) "Polynomial"; (The full theory)

author	berghofe
	Wed, 07 Feb 2007 18:00:38 +0100
changeset 22277	b89dc456dbc6
parent 21256	47195501ecf7
child 24153	1a4607b7ad24
permissions	-rw-r--r--