Return-Path: 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 15:19:15 +0100 Received: by lal.cs.byu.edu (1.38.193.4/16.2) id AA17870; Fri, 30 Sep 1994 08:04:13 -0600 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 lal.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA17866; Fri, 30 Sep 1994 08:03:51 -0600 Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP); Fri, 30 Sep 1994 14:57:25 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <06521-0@i80fs2.ira.uka.de>; Fri, 30 Sep 1994 15:00:24 +0100 Date: Fri, 30 Sep 94 15:00:23 EST From: reetz To: info-hol@lal.cs.byu.edu Cc: slind@informatik.tu-muenchen.de Subject: redirect print_theory from screen into file Message-Id: <"i80fs2.ira.526:30.09.94.14.00.33"@ira.uka.de> Dear all, Does anybody know a fast and easy way to redirect the output of print_theory "xxxx" from the screen into a file for HOL90.6? I just don't want to start trying to "hack around" redirecting std_out or something similiar... Theories are sometimes too large to simply use cut and paste and just a command would be easier, too. In general, it IMHO might be nice to have a changeable io-stream, where HOL90 emits its ``messages'' like in print_theory, theorems, definitions, and so on. Ralf. (**************************************************************) (* *) (* Ralf Reetz *) (* *) (* University of Karlsruhe *) (* Institut fuer Rechnerentwurf und Fehlertoleranz *) (* 76128 Karlsruhe, Zirkel 2, Postfach 6980, Germany *) (* *) (* e-mail: reetz@ira.uka.de *) (* WWW: http://goethe.ira.uka.de/people/reetz/reetz.html *) (* *) (**************************************************************)