| author | nipkow | 
| Wed, 20 Jun 2007 14:38:24 +0200 | |
| changeset 23433 | c2c10abd2a1e | 
| parent 17748 | c93279ba600a | 
| permissions | -rw-r--r-- | 
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> <!-- $Id$ --> <html> <head> <meta http-equiv="content-type" content="text/html;charset=iso-8859-1"> <title>HOL/AxClasses</title> </head> <body> <h1>HOL/AxClasses</h1> These are the HOL examples of the tutorial <a href="http://isabelle.in.tum.de/dist/Isabelle/doc/axclass.pdf">Using Axiomatic Type Classes in Isabelle</a>. See also FOL/ex/NatClass for the natural number example. </body> </html>