Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <09667-0@swan.cl.cam.ac.uk>; Thu, 2 Apr 1992 22:09:56 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA03725;
          Thu, 2 Apr 92 12:46:17 -0800
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Received: from uu.psi.com by ted.cs.uidaho.edu (16.6/1.34) id AA03721;
          Thu, 2 Apr 92 12:46:04 -0800
Received: by uu.psi.com (5.65b/4.1.031792-PSI/PSINet) id AA24963;
          Wed, 1 Apr 92 17:10:04 -0500
Received: from longvalley.cambridge.oracorp.com (longvalley.ARPA) 
          by cambridge.oracorp.com (4.1/3.1.090690-ORA Corporation) id AA11557;
          Wed, 1 Apr 92 16:48:58 EST
Date: Wed, 1 Apr 92 17:02:58 EST
From: weitzman@cambridge.oracorp.com (Adam Weitzman)
Received: by longvalley.cambridge.oracorp.com (4.1/3.1.090690-ORA Corporation) 
          id AA16974; Wed, 1 Apr 92 17:02:58 EST
Message-Id: <9204012202.AA16974@longvalley.cambridge.oracorp.com>
To: info-hol@ted.cs.uidaho.edu
Subject: Theorem conjuncts

Is there any way to take a theorem which is a conjunction of terms and turn
it into a bunch of smaller theorems, each representing one of the
conjuncts? For instance, if I have a theorem:

`big_thm`, |- a /\ b /\ c /\ d

can I make:

`thm_a`, |- a
`thm_b`, |- b
`thm_c`, |- c
`thm_d`, |- d

out of it somehow? The idea is that it is sometimes easier to prove a bunch
of things at once by "and"ing them together and doing STRIP_TAC as soon as
you start the proof, but it would be nice to have each separate theorem in
a separate place once you are done. 

- Adam J Weitzman
  weitzman@canbridge.oracorp.com