--- 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;