Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <13694.9309201133@frogland.inmos.co.uk>
Subject: Re: "hol90.el" (emacs for hol90)
To: info-hol@cs.uidaho.edu (info-hol mailing list)
Date: Mon, 20 Sep 1993 12:33:37 +0100 (BST)
In-Reply-To: <199309151532.AA06404@panther.cs.uidaho.edu> from "Chris Toshok" at Sep 15, 93 08:32:05 am
Content-Type: text
Content-Length: 1940

Chris Toshok has said:
> 
> 
>     Since the hol90 community is constantly growing (:-)
>     there is probably someone in the world who has done
>     a better job in adapting emacs to hol90 and who is
>     willing to share his *.el files.
> 
> Actually, I have been using the sml-mode.el file for hol90.  I just change
> all occurences of sml to hol90 within the elisp file, and it works fine.
> Since hol90 is nothing more than SML/NJ with a lot more definitions added,
> the mode is pretty useful. 

--ditto-- + I've added a some extra indentaion stuff to format tactical proofs
and a couple of functions to autogenerate THEN and THENL's at the correct indentation.

I.e. to prove a theorem

1) set up goal

2) type first tactic then C-c C-c to send it to hol90

3) if get one subgoal type C-c C-t to insert a blank line and
   "THEN " at the correct indentation for then next tactic

   if more than one subgoal type M-x <n> C-c C-T to insert

   THENL
   [

     NO_TAC
    ,
 
     ...
    ,

     NO_TAC
   ]

   as a template at the correct indentation

4) when everyting is solved, edit the top to the relevant prove function
   or whatever, mark a region round the proof, M-TAB collapses all the
   blank lines and (if necessary) C-TAB reindents everything.

Its all a bit hacked (the identation code gets confused by some things in HOL terms)
but it seems to work for me. The other major change was that I modified it to
send small bits of SML direct to the interpreter without using an intermediate
file.

One problem, I think I adapted a fairly elderly version of sml-mode!

--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"They didn't like the rates, they don't like the poll tax,
		 and they won't like the council tax."   - Nicholas Ridley