Remove TABs from examples

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

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!

Added ACL2 quantifiers and other tweaks for the LTL example.

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

Modify a proof so that it works in both
kernels. So sexpScript should build in POLY.

Modifications to allow the translation to run under PolyML.

Modifications to ensure the files work under the experimental kernel.

Fixed various proof scripts in acl2_packageScript.sml and sexpScript.sml so that examples/acl2/ml now builds.

Minor cleanup on sexpScript.sml and added definitions of o_finp, posp,
o_first_expt, and o_first_coeff, which are needed by Matt and
Konrad. They also need o_p and o_less but getting these defined needs
advanced TFL expertise(see commented out proof attempt for the definition
of o_p).

Minor tweaks.

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

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).

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<=.

Minor change and fix to a typo in a comment

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 "".

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.

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

Making sure everything checked in.

(*****************************************************************************)
(* acl2_tgoal "acl2_name" `(foo ... = ...) /\ ... ` creates a termination *)
(* goal for the recursive definition with acl2_name replacing foo. Example: *)
(* *)
(* acl2_tgoal "ACL2::TRUE-LISTP" *)
(* `true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil)` *)
(* *)
(* *)
(*****************************************************************************)

(*****************************************************************************)
(* acl2_defn "acl2_name" (`(foo ... = ...) /\ ... `, tac) uses tac to *)
(* solve the termination goal for the recursive definition with acl2_name *)
(* replacing foo. Makes the definition of acl2_name and then overloads foo *)
(* on acl2_name. Example: *)
(* *)
(* val (true_listp_def,true_listp_ind) = *)
(* acl2_defn "ACL2::TRUE-LISTP" *)
(* (`true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil)`, *)
(* WF_REL_TAC `measure sexp_size` *)
(* THEN RW_TAC arith_ss [sexp_size_cdr]); *)
(*****************************************************************************)

Moving stuff around + some tidying.

Incremental changes (including ``cond`` --> ``ite``).

Getting things to work with the new improved naming scheme.
(e.g. COMMON-LISP::= is now called common_lisp_equal rather than acl2_equal,
and definitions proviously named *_acl2_defun are now stored as *_def).

Interim checkin of current state (various things unfinished).

More support for abbreviating string literals in terms

Have folded package_alistScript.sml into sexpScript.sml and added
some gross hackery to get over what looks to me like a Holmake
compiler bug (see definition of ACL2_PACKAGE_ALIST in sexpScript.sml).

Not sure what's bing checked in .. just did an update to sync everything!

Tidying and bugfixes. example_axioms is in an unfinished state (Matt
suggested more axioms to try to prove, but proofs not yet done).

Minor additions and tidying of existing files. Added an example
showing the importing a few easy ACL2 axioms (suggested by Matt) into
HOL and then proving them as theorems (the clunky treatment is
preliminary and needs to be improved with additional tools).

ML files to support HOL-ACL2 link