Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 5 Oct 1994 08:57:01 +0100 Received: by leopard.cs.byu.edu (1.38.193.4/16.2) id AA16490; Wed, 5 Oct 1994 01:52:50 -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 leopard.cs.byu.edu with SMTP (1.38.193.4/16.2) id AA16484; Wed, 5 Oct 1994 01:52:46 -0600 Received: from i80fs2.ira.uka.de by iraun1.ira.uka.de with SMTP (PP); Wed, 5 Oct 1994 08:46:19 +0100 Received: from ira.uka.de by i80fs2.ira.uka.de id <14030-0@i80fs2.ira.uka.de>; Wed, 5 Oct 1994 08:49:40 +0100 Date: Wed, 5 Oct 94 8:49:39 EST From: reetz To: info-hol@leopard.cs.byu.edu Subject: RE:Re: redirect print_theory from screen into file Message-Id: <"i80fs2.ira.032:05.10.94.07.49.44"@ira.uka.de> Konrad Slind writes: > Separating the different dialogues, perhaps >by use of the ML type system, might be a useful idea. I think so, too. It might be interesting to have an abstract interface between HOL and the user (where the "user" might also be a cad framework or a graphical user interface or pipes or whatever). 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 *) (* *) (**************************************************************)