Some comments added.

--- a/src/Pure/Isar/locale.ML	Mon Aug 02 10:16:40 2004 +0200
+++ b/src/Pure/Isar/locale.ML	Mon Aug 02 10:16:58 2004 +0200
@@ -15,7 +15,7 @@
 
 [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
     In Stefano Berardi et al., Types for Proofs and Programs: International
-    Workshop, TYPES 2003, Torino, Italy, pages ??-??, in press.
+    Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
 *)
 
 signature LOCALE =

--- a/src/Pure/Isar/proof.ML	Mon Aug 02 10:16:40 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Aug 02 10:16:58 2004 +0200
@@ -134,6 +134,13 @@
 
 (* type goal *)
 
+(* CB: three kinds of Isar goals are distinguished:
+   - Theorem: global goal in a theory, corresponds to Isar commands theorem,
+     lemma and corollary,
+   - Have: local goal in a proof, Isar command have
+   - Show: local goal in a proof, Isar command show
+*)
+
 datatype kind =
   Theorem of {kind: string,
     theory_spec: (bstring * theory attribute list) * theory attribute list list,
@@ -142,6 +149,9 @@
   Show of context attribute list list |
   Have of context attribute list list;
 
+(* CB: this function prints the goal kind (Isar command), name and target in
+   the proof state *)
+
 fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _),
         locale_spec = None, view = _}) = s ^ (if a = "" then "" else " " ^ a)
   | kind_name sg (Theorem {kind = s, theory_spec = ((a, _), _),