diff -r 2675e2f4dc61 -r ce0e2b8e8844 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Thu Mar 23 21:36:43 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Thu Mar 23 21:37:13 2000 +0100
@@ -143,6 +143,7 @@
     -> Toplevel.transition -> Toplevel.transition
   val finally_i: (thm list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
+  val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition
   val parse_ast_translation: string -> theory -> theory
   val parse_translation: string -> theory -> theory
   val print_translation: string -> theory -> theory
@@ -454,6 +455,7 @@
 fun also_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.also x);
 fun finally x = proof''' (ProofHistory.applys o gen_calc get_thmss Calculation.finally x);
 fun finally_i x = proof''' (ProofHistory.applys o gen_calc get_thmss_i Calculation.finally x);
+fun moreover comment = proof''' (ProofHistory.apply o Calculation.moreover);
 
 end;