# HG changeset patch
# User wenzelm
# Date 936614979 -7200
# Node ID 9deae880cf740b5715dd956f5018cc17f1133a54
# Parent  5ce623228ef25ba95384540f1430da94955891d6
added README;

diff -r 5ce623228ef2 -r 9deae880cf74 src/Pure/Isar/README
--- /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)
diff -r 5ce623228ef2 -r 9deae880cf74 src/Pure/Thy/README
--- /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)