src/HOL/Isar_examples/README.html
author wenzelm
Sat Sep 04 21:13:01 1999 +0200 (1999-09-04)
changeset 7480 0a0e0dbe1269
parent 7006 46048223e0f9
child 7740 2fbe5ce9845f
permissions -rw-r--r--
replaced ?? by ?;
wenzelm@7005
     1
<!-- $Id$ -->
wenzelm@7005
     2
<html>
wenzelm@7005
     3
wenzelm@7005
     4
<head>
wenzelm@7005
     5
<title>HOL/Isar_examples</title>
wenzelm@7005
     6
</head>
wenzelm@7005
     7
wenzelm@7005
     8
<body>
wenzelm@7005
     9
<h1>HOL/Isar_examples</h1>
wenzelm@7005
    10
wenzelm@7005
    11
Isar offers a new high-level proof (and theory) language interface to
wenzelm@7005
    12
Isabelle.  This directory contains some example Isar documents.  See
wenzelm@7005
    13
the <a href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar page</a>
wenzelm@7005
    14
for more information.
wenzelm@7005
    15
wenzelm@7005
    16
<p>
wenzelm@7005
    17
wenzelm@7006
    18
Note that the theory files are basically just plain ASCII sources of
wenzelm@7006
    19
what are meant to be actual typeset documents.  Automatic LaTeX / PDF
wenzelm@7006
    20
pretty printing will be available in the near future.
wenzelm@7005
    21
wenzelm@7005
    22
<body>
wenzelm@7005
    23
</html>