isabelle: src/HOL/Algebra/ROOT.ML@001323d6d75b (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 *)
14551 2cb6ff394bfb Various changes to HOL-Algebra; ballarin parents: 13949 diff changeset	19	use_thy "Lattice"; (* Lattices, and the complete lattice of subgroups *)
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	20
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	21	(* Rings *)
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	22
13940 c67798653056 HOL-Algebra: New polynomial development added. ballarin parents: 13936 diff changeset	23	use_thy "UnivPoly"; (* Rings and polynomials *)
13936 d3671b878828 Greatly extended CRing. Added Module. ballarin parents: 13870 diff changeset	24
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	25	(*** Old development, based on axiomatic type classes.
0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	26	Will be withdrawn in future. ***)
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	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	29	with_path "poly" (no_document time_use_thy) "Polynomial"; (The full theory)

author	paulson
	Fri, 14 May 2004 16:52:53 +0200
changeset 14748	001323d6d75b
parent 14551	2cb6ff394bfb
child 14751	0d7850e27fed
permissions	-rw-r--r--