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