Pure/Isar/
This directory contains the Isabelle/Isar subsystem -- Intelligible
Semi-Automated Reasoning for Isabelle. Interesting modules include:
ProofContext (structure of Isar proof contexts)
Proof (core of the Isar/VM interpreter)
Args (concrete argument syntax of attributes and methods)
Method (proof methods)
Attrib (attributes)
LocalDefs (local definitions)
Calculation (calculational proofs)
Obtain (generalized existence reasoning)
Toplevel (the Isabelle/Isar toplevel)
IsarThy (Isar derived theory operations)
IsarCmd (non-logical commands)
IsarSyn (syntax for Pure/Isar commands)
OuterParse (outer syntax parser combinators, see also
Pure/General/scan.ML)
OuterSyntax (outer syntax main)
IsarOutput (token-level theory output)