isabelle: src/HOL/Algebra/ROOT.ML@623d4831c8cf (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	(* Preliminaries from set and number theory *)
27713 95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality. ballarin parents: 24153 diff changeset	8	no_document use_thys ["FuncSet", "Primes", "Binomial", "Permutation"];
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20318 diff changeset	9
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	10
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	11	(* New development, based on explicit structures *)
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	12
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	13	use_thys [
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	14	(* Groups *)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	15	"FiniteProduct", (* Product operator for commutative groups *)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	16	"Sylow", (* Sylow's theorem *)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	17	"Bij", (* Automorphism Groups *)
13949 0ce528cd6f19 HOL-Algebra complete for release Isabelle2003 (modulo section headers). ballarin parents: 13943 diff changeset	18
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	19	(* Rings *)
27713 95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality. ballarin parents: 24153 diff changeset	20	"Divisibility", (* Rings *)
95b36bfe7fc4 New locales for orders and lattices where the equivalence relation is not restricted to equality. ballarin parents: 24153 diff changeset	21	"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	22	"UnivPoly" (* Polynomials *)
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	23	];
20318 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
24153 1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	29	no_document use_thys [
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	30	"abstract/Abstract", (The ring theory)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	31	"poly/Polynomial" (The full theory)
1a4607b7ad24 simultaneous use_thys; wenzelm parents: 21256 diff changeset	32	];

author	wenzelm
	Thu, 26 Mar 2009 14:14:02 +0100
changeset 30722	623d4831c8cf
parent 27713	95b36bfe7fc4
child 32480	6c19da8e661a
permissions	-rw-r--r--