Some comments added.
authorballarin
Mon Aug 02 10:16:58 2004 +0200 (2004-08-02)
changeset 150996d8619440ea0
parent 15098 0726e7b15618
child 15100 dfb4e23923e0
Some comments added.
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Mon Aug 02 10:16:40 2004 +0200
     1.2 +++ b/src/Pure/Isar/locale.ML	Mon Aug 02 10:16:58 2004 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  [1] Clemens Ballarin. Locales and Locale Expressions in Isabelle/Isar.
     1.6      In Stefano Berardi et al., Types for Proofs and Programs: International
     1.7 -    Workshop, TYPES 2003, Torino, Italy, pages ??-??, in press.
     1.8 +    Workshop, TYPES 2003, Torino, Italy, LNCS 3085, pages 34-50, 2004.
     1.9  *)
    1.10  
    1.11  signature LOCALE =
     2.1 --- a/src/Pure/Isar/proof.ML	Mon Aug 02 10:16:40 2004 +0200
     2.2 +++ b/src/Pure/Isar/proof.ML	Mon Aug 02 10:16:58 2004 +0200
     2.3 @@ -134,6 +134,13 @@
     2.4  
     2.5  (* type goal *)
     2.6  
     2.7 +(* CB: three kinds of Isar goals are distinguished:
     2.8 +   - Theorem: global goal in a theory, corresponds to Isar commands theorem,
     2.9 +     lemma and corollary,
    2.10 +   - Have: local goal in a proof, Isar command have
    2.11 +   - Show: local goal in a proof, Isar command show
    2.12 +*)
    2.13 +
    2.14  datatype kind =
    2.15    Theorem of {kind: string,
    2.16      theory_spec: (bstring * theory attribute list) * theory attribute list list,
    2.17 @@ -142,6 +149,9 @@
    2.18    Show of context attribute list list |
    2.19    Have of context attribute list list;
    2.20  
    2.21 +(* CB: this function prints the goal kind (Isar command), name and target in
    2.22 +   the proof state *)
    2.23 +
    2.24  fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _),
    2.25          locale_spec = None, view = _}) = s ^ (if a = "" then "" else " " ^ a)
    2.26    | kind_name sg (Theorem {kind = s, theory_spec = ((a, _), _),