src/Pure/Isar/isar_thy.ML
changeset 6774 dec73900168b
parent 6732 cf9f66ca9ee3
child 6850 da8a4660fb0c
     1.1 --- a/src/Pure/Isar/isar_thy.ML	Fri Jun 04 19:54:23 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_thy.ML	Fri Jun 04 19:54:38 1999 +0200
     1.3 @@ -113,6 +113,8 @@
     1.4    val terminal_proof: Method.text * Comment.interest -> Toplevel.transition -> Toplevel.transition
     1.5    val immediate_proof: Toplevel.transition -> Toplevel.transition
     1.6    val default_proof: Toplevel.transition -> Toplevel.transition
     1.7 +  val also: Comment.text -> Toplevel.transition -> Toplevel.transition
     1.8 +  val finally: Comment.text -> Toplevel.transition -> Toplevel.transition
     1.9    val use_mltext: string -> theory option -> theory option
    1.10    val use_mltext_theory: string -> theory -> theory
    1.11    val use_setup: string -> theory -> theory
    1.12 @@ -342,6 +344,18 @@
    1.13  val default_proof = local_default_proof o global_default_proof;
    1.14  
    1.15  
    1.16 +(* calculational proof commands *)
    1.17 +
    1.18 +fun cond_print_calc int thm =
    1.19 +  if int then Pretty.writeln (Pretty.big_list "calculation:" [Display.pretty_thm thm])
    1.20 +  else ();
    1.21 +
    1.22 +fun proof''' f = Toplevel.proof' (f o cond_print_calc);
    1.23 +
    1.24 +fun also _ = proof''' (ProofHistory.applys o Calculation.also);
    1.25 +fun finally _ = proof''' (ProofHistory.applys o Calculation.finally);
    1.26 +
    1.27 +
    1.28  (* use ML text *)
    1.29  
    1.30  fun use_mltext txt opt_thy = #2 (Context.pass opt_thy (use_text false) txt);