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:32:38 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26390;
          Wed, 14 Apr 93 10:12:57 -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 AA26385;
          Wed, 14 Apr 93 10:12:50 -0700
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) to cl; Wed, 14 Apr 1993 18:07:40 +0100
To: Laurent Thery <Laurent.Thery@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 17:51:11 +0100. <"swan.cl.ca.034:14.04.93.16.51.28"@cl.cam.ac.uk>
Date: Wed, 14 Apr 93 18:07:35 +0100
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.373:14.04.93.17.07.49"@cl.cam.ac.uk>


Laurent writes:

> Sorry John, it is not an exception:
> 
> let INDIRECT_TAC = ONCE_REWRITE_TAC[GSYM NOT_CLAUSES] THEN DISCH_TAC;;

Yes indeed -- I stand corrected. However to be pedantic:

> #g "T /\ (a /\ b)";;
> "T /\ a /\ b"
>
> () : void
>
> #e INDIRECT_TAC;;
> OK..
> evaluation failed     DISCH_TAC

you should probably use |PURE_ONCE_REWRITE_TAC|. It can still be described
as a "one-liner".

John.