1(* ===================================================================== *) 2(* FILE : num_conv.sig *) 3(* DESCRIPTION : Signature for the alogical hack relating number *) 4(* constants to their predecessors. Translated from *) 5(* hol88. *) 6(* *) 7(* AUTHOR : Tom Melham *) 8(* TRANSLATOR : Konrad Slind, University of Calgary *) 9(* DATE : September 11, 1991 *) 10(* ===================================================================== *) 11 12 13signature Num_conv = 14sig 15 val num_CONV : Term.term -> Thm.thm 16end 17