Pure/Isar/
This directory contains the Isabelle/Isar subsystem -- Intelligible
Semi-Automated Reasoning for Isabelle. Interesting modules include:
ProofContext (the key concept of Isar proof contexts)
Locale (proof contexts as mathematical structures)
Proof (the Isar/VM proof language interpreter)
Args (concrete argument syntax of attributes and methods)
Method (proof methods)
Attrib (attributes)
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)