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, 28 Feb 1995 08:42:57 +0000
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA094900158;
          Tue, 28 Feb 1995 01:29:18 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from iraun1.ira.uka.de by leopard.cs.byu.edu 
          with SMTP (1.37.109.15/16.2) id AA094320053;
          Tue, 28 Feb 1995 01:27:33 -0700
Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP);
          Tue, 28 Feb 1995 09:25:52 +0100
Received: from ira.uka.de by i80fs2.ira.uka.de id <20110-0@i80fs2.ira.uka.de>;
          Tue, 28 Feb 1995 09:25:44 +0100
Date: Tue, 28 Feb 95 9:25:43 EST
From: reetz <reetz@ira.uka.de>
To: terra@APL.FOX.CS.CMU.EDU
Cc: info-hol@leopard.cs.byu.edu
Subject: re :Need real-world Hol-90 proofs running for 5-60 minutes - forgot 
         seomthing, sorry!
Message-Id: <"i80fs2.ira.112:28.02.95.08.25.47"@ira.uka.de>

Sorry, forgot the literature:

@inproceedings{ReKr94b,
  author      ={{R. Reetz} and {Th. Kropf}},
  title       ={Simplifying Deep Embedding: A Formalised Code Generator},
  booktitle   ={Proc. of the International Workshop on Higher Order Logic
                Theorem Proving and its Applications},
  year        ={1994},
  editor      ={},
  pages       ={378--390},
  organization={},
  publisher   ={Lecture Notes in Computer Science No. 859, Springer},
  address     ={Malta},
  month       ={September},
  note        ={},
  key         ={ReKr94b},
  keyword     ={SFB358 verification compiler HOL},
  remark      ={},
  owner       ={Ralf Reetz}
}


mea culpa, Ralf.