src/Pure/Isar/README
author wenzelm
Fri Apr 07 17:36:25 2000 +0200 (2000-04-07 ago)
changeset 8681 957a5fe9b212
parent 7484 9deae880cf74
child 9124 c702e2125270
permissions -rw-r--r--
apply etc.: comments;
     1 
     2 				Pure/Isar/
     3 
     4 This directory contains the Isabelle/Isar subsystem -- Intelligible
     5 Semi-Automated Reasoning for Isabelle.  Interesting modules include:
     6 
     7   Proof		(core of the Isar/VM interpreter)
     8   Args		(concrete argument syntax of attributes and methods)
     9   Method	(proof methods)
    10   Attrib	(attributes)
    11 
    12   LocalDefs	(local definitions)
    13   Calculation	(calculational proofs)
    14 
    15   Toplevel	(the Isabelle/Isar toplevel)
    16   IsarThy	(Isar derived theory operations)
    17   IsarCmd	(non-logical commands)
    18   IsarSyn	(syntax for Pure/Isar commands)
    19 
    20   OuterParse	(outer syntax parser combinators, see also
    21                  Pure/General/scan.ML)
    22   OuterSyntax   (outer syntax main)