export get_calculation;
authorwenzelm
Sun, 26 Jun 2005 15:16:58 +0200
changeset 16571 c1f41c98fd3c
parent 16570 861b9fa2c98c
child 16572 81778a796290
export get_calculation;
src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sat Jun 25 16:07:55 2005 +0200
+++ b/src/Pure/Isar/calculation.ML	Sun Jun 26 15:16:58 2005 +0200
@@ -7,6 +7,7 @@
 
 signature CALCULATION =
 sig
+  val get_calculation: Proof.state -> thm list option
   val print_global_rules: theory -> unit
   val print_local_rules: Proof.context -> unit
   val trans_add_global: theory attribute