Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Mon, 8 May 1995 21:44:57 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA184145243; Mon, 8 May 1995 11:47:23 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA183365033; Mon, 8 May 1995 11:43:53 -0600 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Mon, 8 May 1995 17:25:32 +0100 To: info-hol@leopard.cs.byu.edu Subject: Mutual induction Date: Mon, 08 May 1995 17:25:24 +0100 From: John Harrison Message-Id: <"swan.cl.cam.:183840:950508162535"@cl.cam.ac.uk> At last I've got round to extending my "alternative" inductive definitions package to handle mutual induction. In the process, I've rewritten almost everything, and integrated the monotonicity prover with the tactic mechanism so that users can lend a hand with monotonicity proofs which don't go through automatically (though almost all do). Interested users can get it from the Cambridge "contrib" area by FTP. At the moment there's only a HOL88 version, but it would be straightforward to port to hol90. ftp.cl.cam.ac.uk hvg/contrib/00-Tarfiles/ind-defs.tar.gz Any comments welcome. John.