Typo.
authorballarin
Tue Aug 03 14:48:59 2004 +0200 (2004-08-03)
changeset 15104f14e0d9587be
parent 15103 79846e8792eb
child 15105 e194d4d265fb
Typo.
src/Provers/Arith/abel_cancel.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Provers/Arith/abel_cancel.ML	Tue Aug 03 14:47:51 2004 +0200
     1.2 +++ b/src/Provers/Arith/abel_cancel.ML	Tue Aug 03 14:48:59 2004 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  signature ABEL_CANCEL =
     1.6  sig
     1.7 -  val ss                : simpset       (*basic simpset of object-logtic*)
     1.8 +  val ss                : simpset       (*basic simpset of object-logic*)
     1.9    val eq_reflection     : thm           (*object-equality to meta-equality*)
    1.10  
    1.11    val sg_ref            : Sign.sg_ref   (*signature of the theory of the group*)
     2.1 --- a/src/Pure/Isar/locale.ML	Tue Aug 03 14:47:51 2004 +0200
     2.2 +++ b/src/Pure/Isar/locale.ML	Tue Aug 03 14:48:59 2004 +0200
     2.3 @@ -732,6 +732,9 @@
     2.4  
     2.5  (* propositions and bindings *)
     2.6  
     2.7 +(* CB: an internal locale (Int) element was either imported or included,
     2.8 +   an external (Ext) element appears directly in the locale. *)
     2.9 +
    2.10  datatype ('a, 'b) int_ext = Int of 'a | Ext of 'b;
    2.11  
    2.12  (* CB: flatten (ids, expr) normalises expr (which is either a locale
    2.13 @@ -1318,6 +1321,7 @@
    2.14  
    2.15  
    2.16  (* predicate text *)
    2.17 +(* CB: generate locale predicates (and delta predicates) *)
    2.18  
    2.19  local
    2.20  
    2.21 @@ -1337,6 +1341,15 @@
    2.22    if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args)
    2.23    else raise Match);
    2.24  
    2.25 +(* CB: define one predicate including its intro rule and axioms
    2.26 +   - bname: predicate name
    2.27 +   - parms: locale parameters
    2.28 +   - defs: thms representing substitutions from defines elements
    2.29 +   - ts: terms representing locale assumptions (not normalised wrt. defs)
    2.30 +   - norm_ts: terms representing locale assumptions (normalised wrt. defs)
    2.31 +   - thy: the theory
    2.32 +*)
    2.33 +
    2.34  fun def_pred bname parms defs ts norm_ts thy =
    2.35    let
    2.36      val sign = Theory.sign_of thy;
    2.37 @@ -1379,6 +1392,11 @@
    2.38          Tactic.compose_tac (false, ax, 0) 1));
    2.39    in (defs_thy, (statement, intro, axioms)) end;
    2.40  
    2.41 +(* CB: modify the locale elements:
    2.42 +   - assume elements become notes elements,
    2.43 +   - notes elements are lifted
    2.44 +*)
    2.45 +
    2.46  fun change_elem _ (axms, Assumes asms) =
    2.47        apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) =>
    2.48          let val (ps,qs) = splitAt(length spec, axs)
    2.49 @@ -1393,6 +1411,8 @@
    2.50  
    2.51  in
    2.52  
    2.53 +(* CB: main predicate definition function *)
    2.54 +
    2.55  fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy =
    2.56    let
    2.57      val (thy', (elemss', more_ts)) =