1(* =====================================================================*) 2(* FILE : mut_rec_ty.sig *) 3(* DESCRIPTION : signature of theorems returned by MutRecDefFunc *) 4(* *) 5(* AUTHOR : Elsa Gunter and Myra VanInwegen, based on comments *) 6(* by Tom Melham *) 7(* DATE : 92.08.08 *) 8(* *) 9(* =====================================================================*) 10 11(* Copyright 1992 by AT&T Bell Laboratories *) 12(* Share and Enjoy *) 13 14signature MutRecDef = 15 sig 16 type thm = Thm.thm 17 18 val define_type 19 : {type_name : string, 20 constructors : {name:string, 21 arg_info : TypeInfo.type_info list}list} list 22 -> 23 {New_Ty_Induct_Thm :thm, 24 New_Ty_Uniqueness_Thm :thm, 25 New_Ty_Existence_Thm :thm} 26 end 27