# 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)) =