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
Subject: Results of the survey on some HOL system libraries
Date: Tue, 05 Oct 93 15:29:36 +0100
From: Wai Wong <Wai.Wong@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:164250:931005143008"@cl.cam.ac.uk>

Thanks to everyone who replied to my questionaire on the more_arithmetic
and more_lists library. As I promised, here is the summary.

There are 13 completed questionaires in total. In addition to
answering the questions, many gave very good suggestions of improving
the libraries, some even sent in new definitions and theorems.
The survey provides very good ideas of what people like, and
will certainly help to improve the libraries. 

I cannot promise to do anything on these libraries right now. Perhaps,
other people can contribute to it.

                     THE RESULTS
                   ================

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

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)
   2 more_arithmetic
   2 add
   2 ineq
   1 min_max
   2 mult
   0 odd_even
   0 pre
   2 sub
   1 suc
   2 zero_ineq

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

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

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)
   1 more_lists
   4 append
   2 el
   4 general_lists
   1 last_subseq
   4 map
   2 member
   0 num_lists
   0 shift
   5 snoc
   2 subseq
   0 tail
   1 unappend
   2 zip

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

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

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

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

10. Would you like to see all definitions and theorems in these
  libraries to be put into the basic system?
   YES 3 /NO 4 /SOME OF THEM 4 /DON'T CARE 2

11. Summary of comments:

	* These two libraries contain very useful stuff, but they need
	  re-organization. 
	* Frequent used definitions and theorems should be moved into
	  the core system.
	* More supports for lists are need.
        * Names of some constants and theorems should be more meaningful.
	* Some means of backward compatibility should be provided when
	  changes are made.


  ______________________________________________________________________