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; Fri, 3 Dec 1993 11:17:23 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA21183;
          Fri, 3 Dec 1993 04:02:46 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA21179;
          Fri, 3 Dec 1993 04:01:47 -0700
Received: from swan.cl.cam.ac.uk by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.4/16.2) id AA13069; Fri, 3 Dec 93 02:58:50 -0800
Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Fri, 3 Dec 1993 10:58:11 +0000
To: info-hol@cs.uidaho.edu
Subject: Re: question about FAUST
Date: Fri, 03 Dec 93 10:58:07 +0000
From: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:048030:931203105814"@cl.cam.ac.uk>


Isabelle's fast_tac solves this problem in about half a second.

							Larry Paulson

> by (fast_tac HOL_cs 1);
Level 1
(! s. q(s) --> r(s)) & ~ r(s) & (! s. ~ r(s) & ~ q(s) --> p(t) | q(t)) -->
p(t) | r(t)
No subgoals!
Process time (incl GC): 0.4 secs