src/HOL/AxClasses/README.html
author nipkow
Wed, 02 Sep 1998 16:52:06 +0200
changeset 5425 157c6663dedd
parent 3279 815ef5848324
child 6215 6165747678ba
permissions -rw-r--r--
Added function upto to List. Had to rearrange loading sequence because now List uses Recdef.

<HTML><HEAD><TITLE>HOL/AxClasses/README</TITLE></HEAD><BODY>

<h2>Axiomatic type classes</h2>

This directory contains the following axiomatic type class examples:


<DL>

<DT> Tutorial
<DD> Some simple axclass demos that go along with the paper <A
HREF="http://www4.informatik.tu-muenchen.de/~nipkow/isadist/axclass.dvi.gz">
"Using Axiomatic Type Classes in Isabelle --- a tutorial". </A>

<P>

<DT> Group
<DD> Some bits of group theory.

<P>

<DT> Lattice
<DD> Basic theory of lattices and orders.

</DL>

</BODY></HTML>