Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Wed, 14 Apr 1993 18:12:16 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26359;
          Wed, 14 Apr 93 09:54:11 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA26354;
          Wed, 14 Apr 93 09:54:03 -0700
Received: from teal.cl.cam.ac.uk (user tl (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Wed, 14 Apr 1993 17:51:19 +0100
To: John Harrison <John.Harrison@uk.ac.cam.cl>
Cc: info-hol@edu.uidaho.cs.ted
Subject: Re: Problem writting INDIRECT_TAC
In-Reply-To: Your message of Wed, 14 Apr 93 16:59:42 +0100. <"swan.cl.ca.151:14.04.93.16.00.00"@cl.cam.ac.uk>
Date: Wed, 14 Apr 93 17:51:11 +0100
From: Laurent Thery <Laurent.Thery@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.038:14.04.93.16.51.32"@cl.cam.ac.uk>

>>   let INDIRECT_TAC (termList, term) =
>>    ( [union [mk_neg term] termList, "F"],
>>      \thmList. CCONTR term (hd thmList));;
>>
>> or
>>
>>  let INDIRECT_TAC (termList, term) =
>>    ( [termList, (mk_imp ((mk_neg term), "F"))],
>>      \thmList. CCONTR term (UNDISCH_ALL(hd thmList)));;
>>
>> This seems to be an exception to the rule that there is usually a trivial way
>> of combining existing tactics, rather than actually writing ML. When I was
>> learning HOL and tried writing my own tactics in ML, I was repeatedly told I
>> was mad.

Sorry John, it is not an exception:

let INDIRECT_TAC = ONCE_REWRITE_TAC[GSYM NOT_CLAUSES] THEN DISCH_TAC;;



--Laurent