# HG changeset patch # User wenzelm # Date 821717441 -3600 # Node ID 7fbe815c18ade0da1406c216fe857a5e7e7afba8 # Parent de6f18da81bb750b11b3dec486fda7b30938838a added Lattice demo; diff -r de6f18da81bb -r 7fbe815c18ad src/HOL/AxClasses/README --- a/src/HOL/AxClasses/README Mon Jan 15 15:49:21 1996 +0100 +++ b/src/HOL/AxClasses/README Mon Jan 15 15:50:41 1996 +0100 @@ -1,10 +1,11 @@ $Id$ -This directory contains some axiomatic type class demos. - +This directory contains the following axiomatic type class examples: Tutorial/ Some simple axclass demos that go along with the paper "Using Axiomatic Type Classes in Isabelle --- a tutorial". - Group/ Basic group theory with axiomatic type classes. + Group/ Some bits of group theory. + + Lattice/ Basic theory of lattices and orders.