# HG changeset patch
# User wenzelm
# Date 1010675068 -3600
# Node ID 77ac6d8451eae46d292fa9e248cc99f66c78d672
# Parent  f0d09c9693d680f39576331f80a9f71f8099fef0
export multi_theorem(_i), locale_multi_theorem(_i);

diff -r f0d09c9693d6 -r 77ac6d8451ea src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Jan 10 13:25:48 2002 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Thu Jan 10 16:04:28 2002 +0100
@@ -96,6 +96,22 @@
     -> bool -> theory -> ProofHistory.T
   val theorem_i: string -> ((bstring * theory attribute list) *
     (term * (term list * term list))) * Comment.text -> bool -> theory -> ProofHistory.T
+  val multi_theorem: string -> bstring * Args.src list ->
+    Args.src Locale.element list ->
+    (((bstring * Args.src list) * (string * (string list * string list)) list)
+      * Comment.text) list -> bool -> theory -> ProofHistory.T
+  val multi_theorem_i: string -> bstring * theory attribute list ->
+    Proof.context attribute Locale.element_i list ->
+    (((bstring * theory attribute list) * (term * (term list * term list)) list)
+      * Comment.text) list -> bool -> theory -> ProofHistory.T
+  val locale_multi_theorem: string -> bstring * Args.src list ->
+    xstring -> Args.src Locale.element list ->
+    (((bstring * Args.src list) * (string * (string list * string list)) list)
+      * Comment.text) list -> bool -> theory -> ProofHistory.T
+  val locale_multi_theorem_i: string -> bstring * theory attribute list ->
+    string -> Proof.context attribute Locale.element_i list ->
+    (((bstring * Proof.context attribute list) * (term * (term list * term list)) list)
+      * Comment.text) list -> bool -> theory -> ProofHistory.T
   val smart_multi_theorem: string -> bstring * Args.src list ->
     xstring Library.option * Args.src Locale.element list ->
     (((bstring * Args.src list) * (string * (string list * string list)) list)
@@ -440,6 +456,8 @@
 fun local_statement f g args = local_statement' (K o f) g args ();
 fun local_statement_i f g args = local_statement_i' (K o f) g args ();
 
+in
+
 fun multi_theorem k a elems args int thy =
   global_statement (Proof.multi_theorem k (apsnd (map (Attrib.global_attribute thy)) a) None
     (map (Locale.attribute (Attrib.local_attribute thy)) elems)) (map Comment.ignore args) int thy;
@@ -458,8 +476,6 @@
       (Some (locale, map (snd o fst o Comment.ignore) args)) elems)
     (map (apfst (apsnd (K [])) o Comment.ignore) args);
 
-in
-
 fun theorem k ((a, t), cmt) = multi_theorem k a [] [((("", []), [t]), cmt)];
 fun theorem_i k ((a, t), cmt) = multi_theorem_i k a [] [((("", []), [t]), cmt)];