Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9403142349.AA03217@puma.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: [Konrad Slind: question about HOL90]
Date: Mon, 14 Mar 1994 16:49:31 -0700
From: Phil Windley <windley@lal.cs.byu.edu>


------- Forwarded Message

From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: info-hol@leopard.cs.byu.edu, semaneth@cis.umassd.edu
Subject: question about HOL90


Sebastian Maneth asks

> I have a little problem with getting HOL90 to run. Also, there might
> be a better ftp-site to download it, than the one I used, since it did
> not have any documentation with it. (I got it from
> research.att.com:/dist/ml/hol) I did get it to run somehow, but none
> of the examples in the HOL book that I have did work. Did the whole
> syntax changed by so much, from HOL88 to HOL90? Where can I get
> documentation for HOL90? (and maybe HOL90 itself, because I think
> there was something wrong with the version from research.att.com )

The quick answer: look in the file doc/{manual,install.doc} of the hol90
release for what meager documentation hol90 has. I believe you will find
answers to your questions there.


The long answer:

There are 2 major differences a user will notice between hol88 and hol90:

    1. hol90 is written in SML/NJ (forcing quotations to be different);
    2. The types of many term manipulation functions have been converted
       from pairs to records.

1.
The major difference in doing simple proofs is probably quotations. In
hol88, a quotation is of the form 

    " ... "  

This is an atomic ML expression and when the ML parser recognizes a
quotation it parses it right away into a term or type. In hol90, a
quotation is of the form 

    ` ... `

This is an atomic SML/NJ expression, and here a difference with ML
manifests itself: the SML/NJ parser decouples application of the term or
type parser from the recognition of the quotation. The user must supply
the parser explicitly, which is a bit of a pain in some ways, and a
great boon in other ways. The basic parsing functions in the "Parse"
structure are "term_parser" and "type_parser". You can use these
directly, but there are "cute" variants that have been dressed up with
some extra syntax so that --`M`-- applies the term parser to "M" and
==`:N`== applies the type parser to "N". If you don't like that syntax,
you can easily substitute some of your own by doing e.g.,

    val % = Parse.term_parser

and then %`A /\ B` is equivalent to --`A /\ B`--


2.
Recordization. In version 5 of hol90, we introduced "record-style"
variants of many common term manipulation functions. For example, a
function like 

    dest_imp: term -> term # term

in hol88 is 

    dest_imp:term -> {ant:term, conseq:term}

in hol90. To get hol88 style term manipulation functions, do the
following: 

    load_library_in_place hol88_lib;
    open Old_syntax Compat;

You are then in a hol88-like setting, bearing in mind that you are still
in SML and quotations are as in (1).


The decision to adopt records was made without consulting the HOL
community, a point that has been made to me many times (usually by John
Harrison). It seems that a reasonable time has passed for people to
decide if they like them. So: what do people think?

Konrad.


------- End of Forwarded Message