src/HOL/Isar_examples/README.html
changeset 7005 cc778d613217
child 7006 46048223e0f9
equal deleted inserted replaced
7004:c799d0859638 7005:cc778d613217
       
     1 <!-- $Id$ -->
       
     2 <html>
       
     3 
       
     4 <head>
       
     5 <title>HOL/Isar_examples</title>
       
     6 </head>
       
     7 
       
     8 <body>
       
     9 <h1>HOL/Isar_examples</h1>
       
    10 
       
    11 Isar offers a new high-level proof (and theory) language interface to
       
    12 Isabelle.  This directory contains some example Isar documents.  See
       
    13 the <a href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a>
       
    14 for more information.
       
    15 
       
    16 <p>
       
    17 
       
    18 Note that the theory files are basically the plain ASCII sources of
       
    19 what is meant to be actual typeset documents.  Automatic LaTeX / PDF
       
    20 pretty printing is not yet available.
       
    21 
       
    22 <body>
       
    23 </html>