summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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.);

2 Pure/Isar/

4 This directory contains the Isabelle/Isar subsystem -- Intelligible

5 Semi-Automated Reasoning for Isabelle. Interesting modules include:

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)

14 LocalDefs (local definitions)

15 Calculation (calculational proofs)

16 Obtain (generalized existence reasoning)

18 Toplevel (the Isabelle/Isar toplevel)

19 IsarThy (Isar derived theory operations)

20 IsarCmd (non-logical commands)

21 IsarSyn (syntax for Pure/Isar commands)

23 OuterParse (outer syntax parser combinators, see also

24 Pure/General/scan.ML)

25 OuterSyntax (outer syntax main)

26 IsarOutput (token-level theory output)