isabelle: src/HOL/Algebra/ROOT.ML@0e0ea63fe768 (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";
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	13
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	14	(* Groups *)
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	use_thy "FiniteProduct"; (* Product operator for commutative groups *)
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	17	use_thy "Sylow"; (* Sylow's theorem *)
13943 83d842ccd4aa moving Bij.thy from GroupTheory to Algebra paulson parents: 13940 diff changeset	18	use_thy "Bij"; (* Automorphism Groups *)
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	19
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	20	(* Rings *)
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	21
13940 c67798653056 HOL-Algebra: New polynomial development added. ballarin parents: 13936 diff changeset	22	use_thy "UnivPoly"; (* Rings and polynomials *)
20318 0e0ea63fe768 Restructured algebra library, added ideals and quotient rings. ballarin parents: 14751 diff changeset	23	use_thy "IntRing"; (* Ideals and residue classes *)
0e0ea63fe768 Restructured algebra library, added ideals and quotient rings. ballarin parents: 14751 diff changeset	24
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	25
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	26	(*** Old development, based on axiomatic type classes.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	27	Will be withdrawn in future. ***)
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	28
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	29	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	30	with_path "poly" (no_document time_use_thy) "Polynomial"; (The full theory)

author	ballarin
	Thu, 03 Aug 2006 14:57:26 +0200
changeset 20318	0e0ea63fe768
parent 14751	0d7850e27fed
child 21256	47195501ecf7
permissions	-rw-r--r--