--- a/src/Provers/Arith/cancel_numerals.ML Fri Apr 22 15:25:01 2011 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML Fri Apr 22 15:57:43 2011 +0200
@@ -42,12 +42,12 @@
val simplify_meta_eq: simpset -> thm -> thm (*simplifies the final theorem*)
end;
+signature CANCEL_NUMERALS =
+sig
+ val proc: simpset -> term -> thm option
+end;
-functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
- sig
- val proc: simpset -> term -> thm option
- end
-=
+functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
struct
(*For t = #n*u then put u in the table*)