--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML Wed Nov 28 12:22:17 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_Reconstruct.ML Wed Nov 28 12:23:44 2012 +0100
@@ -9,7 +9,7 @@
type label = string * int
type facts = label list * string list
-datatype isar_qualifier = Show | Then | Moreover | Ultimately
+datatype isar_qualifier = Show | Then | Ultimately
datatype isar_step =
Fix of (string * typ) list |
@@ -43,4 +43,5 @@
inc (fold (inc o metis_steps_recursive) cases 1)
| _ => I) proof 0
-end
\ No newline at end of file
+
+end