isabelle: src/HOL/Algebra/ROOT.ML@29bb4659f80a (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 *)
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	23
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	24	(*** Old development, based on axiomatic type classes.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	25	Will be withdrawn in future. ***)
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	26
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	27	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	28	with_path "poly" (no_document time_use_thy) "Polynomial"; (The full theory)

author	ballarin
	Tue, 04 Jul 2006 14:47:01 +0200
changeset 19984	29bb4659f80a
parent 14751	0d7850e27fed
child 20318	0e0ea63fe768
permissions	-rw-r--r--