1(* ===================================================================== *) 2(* FILE : Mutual.sig *) 3(* DESCRIPTION : Signature for tools associated with datatypes *) 4(* defined by mutual recursion. *) 5(* We provide an induction tactic, adapted from the *) 6(* standard INDUCT_THEN operator, which was translated *) 7(* from the HOL 88 version. *) 8(* *) 9(* AUTHOR : (c) Tom Melham, University of Cambridge *) 10(* TRANSLATOR : Konrad Slind, University of Calgary *) 11(* ADAPTOR : Peter Vincent Homeier, University of Pennsylvania *) 12(* DATE : March 27, 1998 *) 13(* ===================================================================== *) 14 15 16signature Mutual = 17sig 18 include Abbrev 19 20 val MUTUAL_INDUCT_THEN : thm -> (thm -> tactic) -> tactic 21 val MUTUAL_INDUCT_TAC : thm -> tactic 22end 23