src/HOL/Algebra/README.html
changeset 37435 ed79fa620012
parent 35849 b5522b51cb1e
child 51404 90a598019aeb
equal deleted inserted replaced
37434:df936eadb642 37435:ed79fa620012
    18 The library is expected to grow in future releases of Isabelle.
    18 The library is expected to grow in future releases of Isabelle.
    19 Contributions are welcome.
    19 Contributions are welcome.
    20 
    20 
    21 <H2>GroupTheory, including Sylow's Theorem</H2>
    21 <H2>GroupTheory, including Sylow's Theorem</H2>
    22 
    22 
    23 <P>These proofs are mainly by Florian Kammller.  (Later, Larry
    23 <P>These proofs are mainly by Florian Kamm&uuml;ller.  (Later, Larry
    24 Paulson simplified some of the proofs.)  These theories were indeed
    24 Paulson simplified some of the proofs.)  These theories were indeed
    25 the original motivation for locales.
    25 the original motivation for locales.
    26 
    26 
    27 Here is an outline of the directory's contents: <UL> <LI>Theory <A
    27 Here is an outline of the directory's contents: <UL> <LI>Theory <A
    28 HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,
    28 HREF="Group.html"><CODE>Group</CODE></A> defines semigroups, monoids,