--- a/src/Pure/Isar/README Sat Apr 16 18:58:55 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-
- 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)