Delivery-Date: 
Sender: info-hol-request@cs.uidaho.edu
Errors-To: info-hol-request@cs.uidaho.edu
Precedence: bulk
To: info-hol@cs.uidaho.edu
Cc: Wai.Wong@cl.cam.ac.uk
Subject: A survey on some HOL system libraries
Date: Fri, 03 Sep 93 09:35:22 +0100
From: Wai Wong <Wai.Wong@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:084960:930903083532"@cl.cam.ac.uk>

The more_arithmetic and more_lists libraries have been with HOL88 for
sometime. There have been suggestions to re-organize and to port them
to HOL90. To find out how these libraries are used and to improve
them, may I ask all HOL users to spend a little time to complete the
questionaire below. Please send your reply via E-mail to me at
ww@cl.cam.ac.uk. I'll post a summary of replies in a couple of weeks.
In the same spirit as John Harrison's HOL improvement survey, I'd like
to repeat that we are not committed to accommodating any of the
suggestions, but will certainly consider them. 


                     QUESTIONAIRE
                   ================

1. Have you used the more_arithmethic library?   YES/NO

2. If your answer to Question 1 is YES, please indicate which of
  the theories you have used:
  (if you are not sure, put X against more_arithmetic)
 _______ more_arithmetic
 _______ add
 _______ ineq
 _______ min_max
 _______ mult
 _______ odd_even
 _______ pre
 _______ sub
 _______ suc
 _______ zero_ineq

3. Are you planning to use the more_arithmetic library?  YES/NO

4. Have you used the more_lists library?   YES/NO

5. If your answer to Question 4 is YES, please indicate which of
  the theories you have used:
  (if you are not sure, put X against more_lists)
 _______ more_lists
 _______ append
 _______ el
 _______ general_lists
 _______ last_subseq
 _______ map
 _______ member
 _______ num_lists
 _______ shift
 _______ snoc
 _______ subseq
 _______ tail
 _______ unappend
 _______ zip

6. Are you planning to use the more_lists library?  YES/NO

7. In HOL88, do you prefer that there be no incompatible changes made
  to these libraries?   YES/NO/DON'T CARE

8. Would you be happy to see incompatible changes made to these
  libraries in the port to HOL90? YES/NO/DON'T CARE

9. Do you aware that the arith library has decision procedures for a
  large subset of natural number arithmetic?  YES/NO

10. Would you like to see all definitions and theorems in these
  libraries to be put into the basic system?  YES/NO/SOME OF THEM
  (please indicate what would you like in the basic system)

  ______________________________________________________________________

11. Other comments on these libraries:


  ______________________________________________________________________

------- End of Unsent Draft