--- a/src/HOL/Algebra/README.html Fri Aug 19 21:43:06 2022 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<HTML>
-
-<HEAD>
- <meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
- <TITLE>HOL/Algebra/README.html</TITLE>
-</HEAD>
-
-<BODY>
-
-<H1>Algebra --- Classical Algebra, using Explicit Structures and Locales</H1>
-
-This directory contains proofs in classical algebra. It is intended
-as a base for any algebraic development in Isabelle. Emphasis is on
-reusability. This is achieved by modelling algebraic structures
-as first-class citizens of the logic (not axiomatic type classes, say).
-The library is expected to grow in future releases of Isabelle.
-Contributions are welcome.
-
-<H2>GroupTheory, including Sylow's Theorem</H2>
-
-<P>These proofs are mainly by Florian Kammüller. (Later, Larry
-Paulson simplified some of the proofs.) These theories were indeed
-the original motivation for locales.
-
-Here is an outline of the directory's contents: <UL> <LI>Theory <A
-HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,
-groups, commutative monoids, commutative groups, homomorphisms and the
-subgroup relation. It also defines the product of two groups
-(This theory was reimplemented by Clemens Ballarin).
-
-<LI>Theory <A HREF="FiniteProduct.html"><CODE>FiniteProduct</CODE></A> extends
-commutative groups by a product operator for finite sets (provided by
-Clemens Ballarin).
-
-<LI>Theory <A HREF="Coset.html"><CODE>Coset</CODE></A> defines
-the factorization of a group and shows that the factorization a normal
-subgroup is a group.
-
-<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
-defines bijections over sets and operations on them and shows that they
-are a group. It shows that automorphisms form a group.
-
-<LI>Theory <A HREF="Exponent.html"><CODE>Exponent</CODE></A> the
- combinatorial argument underlying Sylow's first theorem.
-
-<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
-contains a proof of the first Sylow theorem.
-</UL>
-
-<H2>Rings and Polynomials</H2>
-
-<UL><LI>Theory <A HREF="Ring.html"><CODE>CRing</CODE></A>
-defines Abelian monoids and groups. The difference to commutative
- structures is merely notational: the binary operation is
- addition rather than multiplication. Commutative rings are
- obtained by inheriting properties from Abelian groups and
- commutative monoids. Further structures in the algebraic
- hierarchy of rings: integral domain.
-
-<LI>Theory <A HREF="Module.html"><CODE>Module</CODE></A>
-introduces the notion of a R-left-module over an Abelian group, where
- R is a ring.
-
-<LI>Theory <A HREF="UnivPoly.html"><CODE>UnivPoly</CODE></A>
-constructs univariate polynomials over rings and integral domains.
- Degree function. Universal Property.
-</UL>
-
-<H2>Development of Polynomials using Type Classes</H2>
-
-<P>A development of univariate polynomials for HOL's ring classes
-is available at <CODE>HOL/Library/Polynomial</CODE>.
-
-<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
-
-<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
- Author's PhD thesis, 1999. Also University of Cambridge, Computer Laboratory Technical Report number 473.
-
-<ADDRESS>
-<P><A HREF="http://www21.in.tum.de/~ballarin">Clemens Ballarin</A>.
-</ADDRESS>
-</BODY>
-</HTML>