--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/README Mon Sep 06 12:49:39 1999 +0200
@@ -0,0 +1,22 @@
+
+ Pure/Isar/
+
+This directory contains the Isabelle/Isar subsystem -- Intelligible
+Semi-Automated Reasoning for Isabelle. Interesting modules include:
+
+ 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)
+
+ 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)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/README Mon Sep 06 12:49:39 1999 +0200
@@ -0,0 +1,10 @@
+
+ Pure/Thy/
+
+This directory contains the theory loader system, theory presentation
+components, and the parser setup for old-style theory files.
+
+ ThyLoad (theory loader primitives, including load path)
+ ThyInfo (theory loader main)
+ HTML (HTML presentation primitives)
+ ThmDatabase (user-level access to the theorem database)