--- a/src/Pure/Isar/isar_thy.ML Thu Jul 07 12:42:50 2005 +0200
+++ b/src/Pure/Isar/isar_thy.ML Thu Jul 07 15:52:31 2005 +0200
@@ -158,6 +158,8 @@
val register_globally:
((string * Attrib.src list) * Locale.expr) * string option list ->
bool -> theory -> ProofHistory.T
+ val register_in_locale:
+ string * Locale.expr -> bool -> theory -> ProofHistory.T
val register_locally:
((string * Attrib.src list) * Locale.expr) * string option list ->
ProofHistory.T -> ProofHistory.T
@@ -645,6 +647,14 @@
map (fn prop => (prop, ([], []))) props)) propss) int thy'
end;
+fun register_in_locale (target, expr) int thy =
+ let
+ val target = Locale.intern thy target;
+ in
+ locale_multi_theorem_i Drule.internalK target ("",[]) []
+ [] (*concl*) int thy
+ end;
+
fun register_locally (((prfx, atts), expr), insts) =
ProofHistory.apply (fn state =>
let