# HG changeset patch
# User smolkas
# Date 1354101943 -3600
# Node ID 5d6494332b0b29b5ead00a1b3cb1749edc8fdacd
# Parent  1da2e67242d64ada79d8067f7082d2f4deefe6b6
added signature

diff -r 1da2e67242d6 -r 5d6494332b0b src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML	Wed Nov 28 12:25:43 2012 +0100
@@ -6,12 +6,28 @@
 for dealing with Isar proof texts.
 *)
 
-signature SLEDGEHAMMER_Proof =
+signature SLEDGEHAMMER_PROOF =
 sig
-	(* FIXME: TODO *)
+	type label = string * int
+  type facts = label list * string list
+
+  datatype isar_qualifier = Show | Then | Ultimately
+
+  datatype isar_step =
+    Fix of (string * typ) list |
+    Let of term * term |
+    Assume of label * term |
+    Prove of isar_qualifier list * label * term * byline
+  and byline =
+    By_Metis of facts |
+    Case_Split of isar_step list list * facts
+
+  val string_for_label : label -> string
+  val metis_steps_top_level : isar_step list -> int
+  val metis_steps_recursive : isar_step list -> int
 end
 
-structure Sledgehammer_Proof (* : SLEDGEHAMMER_Proof *) = 
+structure Sledgehammer_Proof : SLEDGEHAMMER_PROOF = 
 struct
 
 type label = string * int