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.);
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@12269
     7
  ProofContext  (the key concept of Isar proof contexts)
wenzelm@12269
     8
  Locale        (proof contexts as mathematical structures)
wenzelm@12269
     9
  Proof		(the Isar/VM proof language interpreter)
wenzelm@7484
    10
  Args		(concrete argument syntax of attributes and methods)
wenzelm@7484
    11
  Method	(proof methods)
wenzelm@7484
    12
  Attrib	(attributes)
wenzelm@7484
    13
wenzelm@7484
    14
  LocalDefs	(local definitions)
wenzelm@7484
    15
  Calculation	(calculational proofs)
wenzelm@11020
    16
  Obtain        (generalized existence reasoning)
wenzelm@7484
    17
wenzelm@7484
    18
  Toplevel	(the Isabelle/Isar toplevel)
wenzelm@7484
    19
  IsarThy	(Isar derived theory operations)
wenzelm@7484
    20
  IsarCmd	(non-logical commands)
wenzelm@7484
    21
  IsarSyn	(syntax for Pure/Isar commands)
wenzelm@7484
    22
wenzelm@7484
    23
  OuterParse	(outer syntax parser combinators, see also
wenzelm@7484
    24
                 Pure/General/scan.ML)
wenzelm@7484
    25
  OuterSyntax   (outer syntax main)
wenzelm@9124
    26
  IsarOutput    (token-level theory output)