Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Date: Fri, 17 Jan 92 10:04:14 GMT
Message-Id: <9201171004.AA26024@esat.kuleuven.ac.be>
Original-Received: by esat.kuleuven.ac.be Fri,
                   17 Jan 92 10:04:15 GMT
PP-warning: Illegal Received field on preceding line
From: ploegaer@be.imec
To: info-hol@edu.uidaho.cs.ted
Subject: hol-emacs


Hi!

  I guess a lot of you are using emacs and Phil's beautiful hol-emacs
  mode as the one and only interface to HOL.

  Wrote some more e-lisp code and I'm looking for people that are
  willing to test it (and make comments):

  -1- package to generate the doc-files for theorems and
  ml-identifiers according to standards from guide.tex; The generation
  of the .doc files for theorems is fully automatic (input = result of
  a print_theory). For the other ml-identifiers, there are 3
  functions: creating a .doc "field" containing all entries specified
  in guide.tex (name and type can be inserted automatically); cleaning
  up doc-fields (removing empty, optional entries, protesting against
  required empty entries,...) and installing the doc-fields in the
  appropriate files.

  -2- package based on "occur-mode" to retrieve theorems from a
  theory (based on the name - using some kind of regexps). It searches
  for matching strings in the definition/theorem NAMES in a specified
  theory. It uses a small parser (big word for nothing) such that the
  user does not have to type these strange sequences of "\" himself.
  There are four possibilities:
        -1- find all theorems that contain "string"
        -2- find all theorems that contain "string1" or  "string2"
        (inclusive or)
        -3- find all theorems that contain "string1" and "string2"
        (overlapping with 2, I agree), in whatever order
        -4- find all theorems that contain "string1" followed by
        "string2"

  Both packages are written for GNU emacs 18.57 (and use cl.el)

  A first version of the documentation (LaTeX) is available (I don't
  speak texinfo ...)

  Wim

----------------------------------------------------------------------
Ploegaerts Wim                                e-mail: ploegaer@imec.be
Imec vzw.                                     Tel.:   (32) 16/281 525
Kapeldreef 75                                 Fax.:   (32) 16/281 515
3001   Leuven,  Belgium                       Telex:  26.152