# HG changeset patch
# User ballarin
# Date 1091537339 -7200
# Node ID f14e0d9587bec6362b2d4ebd89d868445c5dc2ea
# Parent  79846e8792ebcfb3abe0ac55a1c5a19f63673f22
Typo.

diff -r 79846e8792eb -r f14e0d9587be src/Provers/Arith/abel_cancel.ML
--- a/src/Provers/Arith/abel_cancel.ML	Tue Aug 03 14:47:51 2004 +0200
+++ b/src/Provers/Arith/abel_cancel.ML	Tue Aug 03 14:48:59 2004 +0200
@@ -14,7 +14,7 @@
 
 signature ABEL_CANCEL =
 sig
-  val ss                : simpset       (*basic simpset of object-logtic*)
+  val ss                : simpset       (*basic simpset of object-logic*)
   val eq_reflection     : thm           (*object-equality to meta-equality*)
 
   val sg_ref            : Sign.sg_ref   (*signature of the theory of the group*)
diff -r 79846e8792eb -r f14e0d9587be src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Aug 03 14:47:51 2004 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Aug 03 14:48:59 2004 +0200
@@ -732,6 +732,9 @@
 
 (* propositions and bindings *)
 
+(* CB: an internal locale (Int) element was either imported or included,
+   an external (Ext) element appears directly in the locale. *)
+
 datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
 
 (* CB: flatten (ids, expr) normalises expr (which is either a locale
@@ -1318,6 +1321,7 @@
 
 
 (* predicate text *)
+(* CB: generate locale predicates (and delta predicates) *)
 
 local
 
@@ -1337,6 +1341,15 @@
   if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
   else raise Match);
 
+(* CB: define one predicate including its intro rule and axioms
+   - bname: predicate name
+   - parms: locale parameters
+   - defs: thms representing substitutions from defines elements
+   - ts: terms representing locale assumptions (not normalised wrt. defs)
+   - norm_ts: terms representing locale assumptions (normalised wrt. defs)
+   - thy: the theory
+*)
+
 fun def_pred bname parms defs ts norm_ts thy =
   let
     val sign = Theory.sign_of thy;
@@ -1379,6 +1392,11 @@
         Tactic.compose_tac (false, ax, 0) 1));
   in (defs_thy, (statement, intro, axioms)) end;
 
+(* CB: modify the locale elements:
+   - assume elements become notes elements,
+   - notes elements are lifted
+*)
+
 fun change_elem _ (axms, Assumes asms) =
       apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
         let val (ps,qs) = splitAt(length spec, axs)
@@ -1393,6 +1411,8 @@
 
 in
 
+(* CB: main predicate definition function *)
+
 fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
   let
     val (thy', (elemss', more_ts)) =