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; Thu, 23 Jun 1994 16:21:18 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA04135; Thu, 23 Jun 1994 08:48:29 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from irafs1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA04128; Thu, 23 Jun 1994 08:48:04 -0600 Received: from i80fs2.ira.uka.de (actually i80fs2) by irafs1 with SMTP (PP); Thu, 23 Jun 1994 16:40:50 +0200 Received: from ira.uka.de by i80fs2.ira.uka.de id <01046-0@i80fs2.ira.uka.de>; Thu, 23 Jun 1994 16:47:45 +0200 Date: Thu, 23 Jun 94 16:47:44 EDT From: reetz To: info-hol@leopard.cs.byu.edu Subject: How do I extend hol90.6's pretty printer? Message-Id: <"i80fs2.ira.048:23.05.94.14.47.48"@ira.uka.de> I would like to extend the pretty printer of hol90.6 to pretty-print some sort of terms, e.g. I have defined an infix "sappend" and would like to get it pretty-printed as "^". Or another example: Assume I have a function fun my_term_2_string: term -> string, which takes a term of a certain type and transforms the term into a string. If the term has not the certain type, it will fail. I would like to extend the pretty-printer by this function. Frankly, I have absolutely no idea on how to do it and the existing readme's confused me completely. Can anybody loose some words on how to do these things? Thank you a lot in advance! Ralf. (*****************************************************************************) (* *) (* Ralf Reetz SFB 358 of the german research *) (* reetz@ira.uka.de society (DFG) *) (* reetz@informatik.uni-karlsruhe.de University of Karlsruhe, Germany *) (* *) (*****************************************************************************)