# HG changeset patch
# User wenzelm
# Date 1005511134 -3600
# Node ID fb0fb0209c87660ef237cac8d7838ee8680335b5
# Parent  f83dc4202b78dc12ce501f7a84d6ead6f85870a1
present multi_result;

diff -r f83dc4202b78 -r fb0fb0209c87 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sun Nov 11 21:38:25 2001 +0100
+++ b/src/Pure/Thy/html.ML	Sun Nov 11 21:38:54 2001 +0100
@@ -34,7 +34,7 @@
     (Url.T option * Url.T * bool option) list -> text -> text
   val end_theory: text
   val ml_file: Url.T -> string -> text
-  val result: string -> string -> thm -> text
+  val multi_result: string * (string * thm list) list -> text
   val results: string -> string -> thm list -> text
   val theorem: string -> thm -> text
   val theorems: string -> thm list -> text
@@ -277,10 +277,13 @@
 
 in
 
-fun result k a th = para (keyword k ^ thm_name a ^ "\n" ^ thm th);
 fun results k a ths = para (cat_lines ((keyword k ^ thm_name a) :: map thm ths));
 
-val theorem = result "theorem";
+fun multi_result (_, []) = ""
+  | multi_result (k, ((a, ths) :: res)) =
+      cat_lines (results k a ths :: map (uncurry (results "and")) res);
+
+fun theorem a th = multi_result ("theorem", [(a, [th])]);
 val theorems = results "theorems";
 
 end;
diff -r f83dc4202b78 -r fb0fb0209c87 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Nov 11 21:38:25 2001 +0100
+++ b/src/Pure/Thy/present.ML	Sun Nov 11 21:38:54 2001 +0100
@@ -25,7 +25,7 @@
   val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
   val theory_output: string -> string -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
-  val result: string -> string -> thm -> unit
+  val multi_result: string * (string * thm list) list -> unit
   val results: string -> string -> thm list -> unit
   val theorem: string -> thm -> unit
   val theorems: string -> thm list -> unit
@@ -466,7 +466,7 @@
   end);
 
 
-fun result k a thm = with_session () (fn _ => with_context add_html (HTML.result k a thm));
+fun multi_result res = with_session () (fn _ => with_context add_html (HTML.multi_result res));
 fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms));
 fun theorem a thm = with_session () (fn _ => with_context add_html (HTML.theorem a thm));
 fun theorems a thms = with_session () (fn _ => with_context add_html (HTML.theorems a thms));