src/HOL/AxClasses/README
author paulson
Fri, 22 Dec 1995 10:26:57 +0100
changeset 1413 73fac49f608f
parent 1265 6ef9a9893fd6
child 1441 7fbe815c18ad
permissions -rw-r--r--
"prepare_proof" has been simplified because rewrite_rule and rewrite_goals_rule check for empty lists. The list of premises is *not* passed to Thm.compress; this was tried, but the potential storage gains seemed not to justify the cpu time required.

$Id$

This directory contains some axiomatic type class demos.


  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.