src/Pure/Isar/README
author wenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 7632 25a0d2ba3a87
parent 7484 9deae880cf74
child 9124 c702e2125270
permissions -rw-r--r--
removed extra shyps error;
     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)