added also, finally;
authorwenzelm
Fri Jun 04 19:54:38 1999 +0200 (1999-06-04 ago)
changeset 6774dec73900168b
parent 6773 83c09a9684cf
child 6775 9d96ce9c27d6
added also, finally;
src/Pure/Isar/isar_thy.ML
     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);