# HG changeset patch
# User wenzelm
# Date 928518878 -7200
# Node ID dec73900168bf193acd55966e239924c59773901
# Parent  83c09a9684cf50e2c1ba5324c7a7f516821dfe11
added also, finally;

diff -r 83c09a9684cf -r dec73900168b src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Fri Jun 04 19:54:23 1999 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Fri Jun 04 19:54:38 1999 +0200
@@ -113,6 +113,8 @@
   val terminal_proof: Method.text * Comment.interest -> Toplevel.transition -> Toplevel.transition
   val immediate_proof: Toplevel.transition -> Toplevel.transition
   val default_proof: Toplevel.transition -> Toplevel.transition
+  val also: Comment.text -> Toplevel.transition -> Toplevel.transition
+  val finally: Comment.text -> Toplevel.transition -> Toplevel.transition
   val use_mltext: string -> theory option -> theory option
   val use_mltext_theory: string -> theory -> theory
   val use_setup: string -> theory -> theory
@@ -342,6 +344,18 @@
 val default_proof = local_default_proof o global_default_proof;
 
 
+(* calculational proof commands *)
+
+fun cond_print_calc int thm =
+  if int then Pretty.writeln (Pretty.big_list "calculation:" [Display.pretty_thm thm])
+  else ();
+
+fun proof''' f = Toplevel.proof' (f o cond_print_calc);
+
+fun also _ = proof''' (ProofHistory.applys o Calculation.also);
+fun finally _ = proof''' (ProofHistory.applys o Calculation.finally);
+
+
 (* use ML text *)
 
 fun use_mltext txt opt_thy = #2 (Context.pass opt_thy (use_text false) txt);