--- a/src/Pure/Isar/isar_thy.ML Sun Mar 26 22:29:33 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML Sun Mar 26 22:31:11 2000 +0200
@@ -144,6 +144,7 @@
val finally_i: (thm list * Comment.interest) option * Comment.text
-> Toplevel.transition -> Toplevel.transition
val moreover: Comment.text -> Toplevel.transition -> Toplevel.transition
+ val ultimately: 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
@@ -456,6 +457,7 @@
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);
+fun ultimately comment = proof''' (ProofHistory.apply o Calculation.ultimately);
end;