src/Pure/Isar/README
author wenzelm
Wed Dec 05 03:18:03 2001 +0100 (2001-12-05 ago)
changeset 12385 389d11fb62c8
parent 12269 fda9192d0344
child 14579 e79f1923fa0a
permissions -rw-r--r--
removed unused functionality (weight etc.);
     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   ProofContext  (the key concept of Isar proof contexts)
     8   Locale        (proof contexts as mathematical structures)
     9   Proof		(the Isar/VM proof language interpreter)
    10   Args		(concrete argument syntax of attributes and methods)
    11   Method	(proof methods)
    12   Attrib	(attributes)
    13 
    14   LocalDefs	(local definitions)
    15   Calculation	(calculational proofs)
    16   Obtain        (generalized existence reasoning)
    17 
    18   Toplevel	(the Isabelle/Isar toplevel)
    19   IsarThy	(Isar derived theory operations)
    20   IsarCmd	(non-logical commands)
    21   IsarSyn	(syntax for Pure/Isar commands)
    22 
    23   OuterParse	(outer syntax parser combinators, see also
    24                  Pure/General/scan.ML)
    25   OuterSyntax   (outer syntax main)
    26   IsarOutput    (token-level theory output)