| 15283 |      1 | <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
 | 
|  |      2 | 
 | 
| 7005 |      3 | <html>
 | 
|  |      4 | 
 | 
|  |      5 | <head>
 | 
| 15582 |      6 |   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
 | 
| 33026 |      7 |   <title>HOL/Isar_Examples</title>
 | 
| 7005 |      8 | </head>
 | 
|  |      9 | 
 | 
|  |     10 | <body>
 | 
| 33026 |     11 | <h1>HOL/Isar_Examples</h1>
 | 
| 7005 |     12 | 
 | 
|  |     13 | Isar offers a new high-level proof (and theory) language interface to
 | 
|  |     14 | Isabelle.  This directory contains some example Isar documents.  See
 | 
| 7804 |     15 | also the included document, or the <a
 | 
|  |     16 | href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a> for more
 | 
|  |     17 | information.
 | 
|  |     18 | </body>
 | 
| 7005 |     19 | </html>
 |