Reconcile store_thms with diverging names in db and val binding

Remove TABs from examples

New goalstack pretty-printing trace & rationalise goalstack trace names

New trace prints a count of the sub-goals at the end of the stack.
This saves the user from having to scroll back over the several
hundred goals they've just generated to find out the number.

Repaired proofs broken due to inconsistent witness selection across versions.

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Various updates, tweaks and fixes in preparation for Matt's visit

Modifications to ensure the files work under the experimental kernel.

Complete rework of the function encoding for ACL2. Usage of the encoding is
contained in acl2encodeLib.sig.

hol_defaxioms_proofsScript : Updated to run under the experimental kernel

Fixes to get things to work after recent changed to HOL4
(theorem deletions; tags->strings)

Fixed some minor issues that came up when Matt checked that the ACL2
axioms verified in HOL were indeed the ACL2 axioms. The axioms are now
confirmed as verified.

Minor tweaks.

Proof of most (maybe all) of the remaining ACL2 axioms.

Making sure CVS repository is consistent. Hope this fixes a build problem.

Proof of another couple of ACL2 axioms. Exported some theorems proved in
translateScript.sml that were useful in hol_defaxioms_proofsScript.sml.

Proof (and supporting lemmas) of a few more ACL2 axioms. Some turned
out to be false and needed a change to the definition of pkg_witness
in sexpScript.sml (the false axiom revealed a soundness bug in ACL2,
which has now been fixed by Matt Kaufmann).

A few more ACL2 axioms proved + some supporting lemmas
(several taken from translateScript.sml).

More stuff towards proving the ACL2 axiom.

More progress towards proving the ACL2 axioms.

Another ACL2 axiom proved. Needed a change to the definition of
ACL2::BAD-ATOM<=.

Proved another ACL2 axiom. This one revealed a soundness bug in ACL2
(rapidly fixed by Matt, see below) who writes:

I looked into this I found that ACL2 has a related soundness bug!
As the next release note will explain:

Fixed a soundness bug in handling of primitive function pkg-witness.
(The executable counterpart returned an incorrect default value.)

Matt added the following comment to axioms.lisp:

; Essay on Symbols and Packages

; A symbol may be viewed as a pair consisting of two strings: its symbol-name
; and its symbol-package-name, where the symbol-package-name is not "". (A
; comment in intern-in-package-of-symbol-symbol-name discusses why we disallow
; "".) However, some such pairs are not symbols because of the import
; structure (represented in world global 'known-package-alist). For example,
; the "ACL2" package imports a symbol with symbol-name "CAR" from the
; "COMMON-LISP" package, so the symbol-package-name of ACL2::CAR is
; "COMMON-LISP". Thus there is no symbol with a symbol-name of "CAR" and a
; symbol-package-name of "ACL2".

; The package system has one additional requirement: No package is allowed to
; import any symbol named *pkg-witness-name* from any other package. The
; function pkg-witness returns a symbol with that name; moreover,
; the symbol-package-name of (pkg-witness p) is p if p is a string, else is
; "ACL2".

; Logically, we imagine that a package exists for every string (serving as the
; symbol-package-name of its symbols) except "". Of course, at any given time
; only finite many packages have been specified (either being built-in, or
; specified with defpkg); and, ACL2 will prohibit explicit specification of
; packages for certain strings, such as "ACL2_INVISIBLE".

; Finally, we specify that the symbol-name and symbol-package-name of any
; non-symbol are "".

Another ACL2 axiom proved.

Added a stub (hol_defaxioms_thmsScript.sml) to contain proofs of
defthms in axioms.lisp. Also a few more proofs of ACL2 axioms (still a
long way to go alas).

Also added (failed) attempt to get HOL to accept character literals
directly (i.e. without an antiquotation hack). Still have problems
with standard_char_p_def in hol_defaxiomsScript.sml.

Various updates.

A little progress and on proving the ACL2 axioms.

Beginnings of proof of ACL2 axioms (+ tweaks to existing stuff).