Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from lal.cs.byu.edu (actually leopard.cs.byu.edu !OR! info-hol-request@lal.cs.byu.edu) 
          by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk;
          Fri, 30 Sep 1994 17:09:02 +0100
Received: by lal.cs.byu.edu (1.38.193.4/16.2) id AA20118;
          Fri, 30 Sep 1994 10:02:36 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from vanuata.dcs.gla.ac.uk by lal.cs.byu.edu 
          with SMTP (1.38.193.4/16.2) id AA20108;
          Fri, 30 Sep 1994 10:02:30 -0600
Received: from switha.dcs.gla.ac.uk by vanuata.dcs.gla.ac.uk with SMTP (PP);
          Fri, 30 Sep 1994 16:56:10 +0100
To: reetz <reetz@ira.uka.de>
Cc: info-hol@lal.cs.byu.edu, slind@informatik.tu-muenchen.de, tfm@dcs.gla.ac.uk
Subject: Re: redirect print_theory from screen into file
In-Reply-To: Your message of "Fri, 30 Sep 1994 15:00:23 EST." <"i80fs2.ira.526:30.09.94.14.00.33"@ira.uka.de>
Date: Fri, 30 Sep 1994 16:56:07 +0100
From: "Tom. F. Melham" <tfm@dcs.gla.ac.uk>
Message-ID: <"swan.cl.cam.:067220:940930160940"@cl.cam.ac.uk>

Personally, I would just run a file containing

   print_theory `foo`;;

through HOL as a background job and redirect the output to a file:

   hol < file.ml > printed-stuff

Or else I'd run print_theory in an emacs window and save the results
that way. But this low-tech solution probably wouldn't satisfy many
people...

Tom