Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Tue, 10 Nov 1992 09:02:42 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA29269; Tue, 10 Nov 92 00:29:38 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA29264; Tue, 10 Nov 92 00:29:32 -0800 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA18986; Tue, 10 Nov 92 00:28:52 -0800 Message-Id: <9211100828.AA18986@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted Cc: chou@edu.ucla.cs Subject: A little problem Date: Tue, 10 Nov 92 00:28:51 PST From: chou@edu.ucla.cs As we all know, the HOL quotation parser often needs quite a few type annotations to be able to type-check a term. A common way of avoiding explicitly writing too many type annotations is to use anti-quotations. But to use anti-quotations, one needs to bind ML identifiers to HOL logic types or terms. Unfortunately, ML bindings does not persist from one HOL session to another. This means that one has to do the ML bindings anew for every a new HOL session, which can become very tedious. I wonder whether there is an easier way to solve this little problem. - Ching Tsun