--- a/src/Pure/Isar/README Thu Nov 22 17:14:17 2001 +0100
+++ b/src/Pure/Isar/README Thu Nov 22 23:15:12 2001 +0100
@@ -4,8 +4,9 @@
This directory contains the Isabelle/Isar subsystem -- Intelligible
Semi-Automated Reasoning for Isabelle. Interesting modules include:
- ProofContext (structure of Isar proof contexts)
- Proof (core of the Isar/VM interpreter)
+ 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)