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