Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 9 Jun 1994 19:42:59 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA22397;
          Thu, 9 Jun 1994 12:30:48 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from vanuata.dcs.gla.ac.uk by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA22393;
          Thu, 9 Jun 1994 12:30:46 -0600
Received: from switha.dcs.gla.ac.uk by goggins.dcs.gla.ac.uk 
          with LOCAL SMTP (PP) id <25483-0@goggins.dcs.gla.ac.uk>;
          Thu, 9 Jun 1994 19:29:01 +0100
Received: by switha.dcs.gla.ac.uk (4.1/Dumb) id AA11768;
          Thu, 9 Jun 94 19:28:59 BST
From: tfm@dcs.gla.ac.uk
Message-Id: <9406091828.AA11768@switha.dcs.gla.ac.uk>
To: info-hol@leopard.cs.byu.edu
Cc: tfm@dcs.gla.ac.uk
Subject: ind_defs library in HOL88 version 2.02.
Date: Thu, 09 Jun 94 19:28:59 +0100


I'm afraid that one of the changes made to HOL88 version 2.02
has broken the function 

    derive_cases_thm
 
in my ind_defs library.  Wai Wong modified the MP rule so that
it no longer does

       |- ~P     |- P
   ----------------------   MP
           |- F

by treating |- ~P as |- P ==> F.  I'm afraid I have been     
deliberately using this feature for a long time now, and in
particular my ind_defs implementation used it in a few places.

The quick-and-easy fix is to locally restore the old meaning of
MP within the ind-defs.ml file in the ind_defs library.  Insert
the code

   let MP th1 th2 =
       if (is_neg(concl th1)) then
          MP (NOT_ELIM th1) th2 else MP th1 th2;;

just after the definition of MATCH_MP within the section for
derive_cases_thm and recompile.

Best wishes,
Tom Melham