src/HOL/README.html
changeset 7303 96bc013c8987
parent 7291 8aa66ddc0bea
child 7662 062a782d7402
     1.1 --- a/src/HOL/README.html	Fri Aug 20 15:34:51 1999 +0200
     1.2 +++ b/src/HOL/README.html	Fri Aug 20 15:41:19 1999 +0200
     1.3 @@ -14,6 +14,21 @@
     1.4  <DT>Auth
     1.5  <DD>a new approach to verifying authentication protocols 
     1.6  
     1.7 +<DT>AxClasses
     1.8 +<DD>a few axiomatic type class examples:
     1.9 +<DL>
    1.10 +
    1.11 +<DT> Tutorial <DD> Some simple axclass demos that go along with the
    1.12 +<em>axclass</em> Isabelle document (<tt>isatool doc axclass</tt>).
    1.13 +
    1.14 +<DT> Group
    1.15 +<DD> Some bits of group theory.
    1.16 +
    1.17 +<DT> Lattice
    1.18 +<DD> Basic theory of lattices and orders.
    1.19 +
    1.20 +</DL>
    1.21 +
    1.22  <DT>Hoare
    1.23  <DD>verification of imperative programs; verification conditions are
    1.24  generated automatically from pre/post conditions and loop invariants.
    1.25 @@ -31,6 +46,9 @@
    1.26  <DT>IOA
    1.27  <DD>a simple theory of Input/Output Automata
    1.28  
    1.29 +<DT>Isar_examples
    1.30 +<DD>some Isabelle/Isar proof documents
    1.31 +
    1.32  <DT>Lambda
    1.33  <DD>a proof of the Church-Rosser theorem for lambda-calculus
    1.34