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