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 tweaks (some ugly) to get things working again.

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

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

Adjusting the handling of encapsulate + stuff for a small test example.

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

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

More progress towards proving the ACL2 axioms.

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

Another ACL2 axiom proved.

Updated to demonstrate that the nice version of the definition is possible.

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

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]); *)
(*****************************************************************************)

Tweaked acl2_name_to_hol_name to eliminate occurrences of "__".

Replace the temporary acl2_defs_theory by hol_defaxiomsTheory.

Initially hol_defaxiomsScript.sml started as a list of desired
definitions (and -- later in the file -- theorems) imported from
ACL2. The imported desired stuff is in the comments.

For example, after the boilerplate, hol_defaxiomsScript.sml starts
with:

(*
[oracles: DEFUN ACL2::IFF, DISK_THM] [axioms: ] []
|- iff p q = itel [(p,andl [q; t]); (q,nil)] t,
*)

This comment contains a printout of a theorem created by trusting ACL2
(see added tag, which indicates that DEFUN is trusted and showing the
ACL2 name). The long-term goal is to eliminate the need to trust ACL2 when
defining the core ACL2 theory. Thus we have the pure HOL definition:

val iff_def =
acl2Define "ACL2::IFF"
`iff p q = itel [(p,andl [q; t]); (q,nil)] t`;

So far we have only made HOL definitions of those functions
immediately needed (e.g. by James' translate tool).

Sometimes, for historical reasons, we define a function slightly
different from the definition in the comment (e.g. see ACL2::ZP) and
then prove that the definition made implements the one in the comment.

Eventually desired recursive definitions will be needed. So far
acl2Define doesn't support this well, so we have the interim
implementation of

(*
[oracles: DEFUN ACL2::TRUE-LISTP, DISK_THM] [axioms: ] []
|- true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil),
*)

implemented as:

val (true_listp_def,true_listp_ind) =
Defn.tprove
(Hol_defn
"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]);

but eventually we need the constant to be named "ACL2::TRUE-LISTP",
and "true_lisp" is just overloaded onto that.

Once all the definitions have been made, we hope to prove the ACL2
axioms, thereby establishing that we have a model of the ACL2
theory. This may be a lot of work though.

Partial definition of functions imported from ACL2's axioms.lisp in HOL.
Work in progress. Should eventually replace the ad hoc acl2_defsScript.sml