Structure Num_conv

(* ===================================================================== *)
(* FILE          : num_conv.sig                                          *)
(* DESCRIPTION   : Signature for the alogical hack relating number       *)
(*                 constants to their predecessors. Translated from      *)
(*                 hol88.                                                *)
(*                                                                       *)
(* AUTHOR        : Tom Melham                                            *)
(* TRANSLATOR    : Konrad Slind, University of Calgary                   *)
(* DATE          : September 11, 1991                                    *)
(* ===================================================================== *)


signature Num_conv =
sig
   val num_CONV : Term.term -> Thm.thm
end

HOL 4, Kananaskis-14