tuned signature;
authorwenzelm
Fri Apr 22 15:57:43 2011 +0200 (2011-04-22)
changeset 424620fd80c27fdf5
parent 42461 56975de9e341
child 42463 f270e3e18be5
tuned signature;
src/Provers/Arith/cancel_numerals.ML
     1.1 --- a/src/Provers/Arith/cancel_numerals.ML	Fri Apr 22 15:25:01 2011 +0200
     1.2 +++ b/src/Provers/Arith/cancel_numerals.ML	Fri Apr 22 15:57:43 2011 +0200
     1.3 @@ -42,12 +42,12 @@
     1.4    val simplify_meta_eq: simpset -> thm -> thm    (*simplifies the final theorem*)
     1.5  end;
     1.6  
     1.7 +signature CANCEL_NUMERALS =
     1.8 +sig
     1.9 +  val proc: simpset -> term -> thm option
    1.10 +end;
    1.11  
    1.12 -functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA):
    1.13 -  sig
    1.14 -  val proc: simpset -> term -> thm option
    1.15 -  end
    1.16 -=
    1.17 +functor CancelNumeralsFun(Data: CANCEL_NUMERALS_DATA): CANCEL_NUMERALS =
    1.18  struct
    1.19  
    1.20  (*For t = #n*u then put u in the table*)