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; Tue, 26 Sep 1995 13:40:56 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA025007476;
          Tue, 26 Sep 1995 06:11:16 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from bunsen.cs.byu.edu by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA024977474;
          Tue, 26 Sep 1995 06:11:14 -0600
Received: from vanuata.dcs.gla.ac.uk (vanuata.dcs.gla.ac.uk [130.209.240.50]) 
          by bunsen.cs.byu.edu (8.6.9/8.6.9) with ESMTP id GAA18221 
          for <info-hol@cs.byu.edu>; Tue, 26 Sep 1995 06:10:40 -0600
Message-Id: <199509261210.GAA18221@bunsen.cs.byu.edu>
Received: from gozo.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with LOCAL SMTP (PP);
          Tue, 26 Sep 1995 12:48:11 +0100
To: Lawrence C Paulson <Larry.Paulson@cl.cam.ac.uk>
Cc: John Harrison IB <jharriso@ra.abo.fi>, info-hol@cs.byu.edu, 
    isabelle-users@cl.cam.ac.uk, tfm@dcs.gla.ac.uk
Subject: Re: At a Los for something to do? (II)
In-Reply-To: Your message of "Tue, 26 Sep 1995 11:44:15 BST." <"swan.cl.cam.:144290:950926104427"@cl.cam.ac.uk>
Date: Tue, 26 Sep 1995 12:48:03 +0100
From: Tom Melham <tfm@dcs.gla.ac.uk>


> safe_meson_tac works by the so-called MESON proof procedure, which is a 
> sequent formulation of Model Elimination.

Got an accessible reference?

Tom