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

Final raft of compatlibility changes.

Modifications to allow the translation to run under PolyML.

Attempt to get my local version in sync with repository copy. If
it causes trouble for others, I can fix in the next few days.

bugfix

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

Update the type of mk_oracle_thm so that it takes a string rather than a
tag as first argument. This is to prevent the following scenario:

- show_tags := true;
> val it = () : unit

- val ax = new_axiom ("foo", ``T``);
> val ax = [oracles: ] [axioms: foo] [] |- T : thm

- val th = mk_oracle_thm (Thm.tag ax) ([], ``F``);
> val th = [oracles: ] [axioms: foo] [] |- F : thm

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

Making sure SF state is up to date with lates encapsulate stuff.

Interim checkin. Some code reorganised and preliminary support for ACL2
ENCAPSULATE and MUTUAL-RECURSION events added.

encodeLib: Now handles lambda abstractions and let syntax natively
Improved support for difficult recursion schemes (eg. DIV)
translateScript: Added translations for strings and characters
Definitions are now checked one by one to avoid the
'couldn't protect' error
sexp: Added support for 'let a = b and c = d in...' syntax

Tweaks: temporarily disabled ACL2 invocation (not working on my machine).
Updated README + comment typo fixes in sexp.sml.

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.

Various updates.

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

Minor tweaks and updates.

Tidying up. Note that acl2_defsTheory replaces basic_defaxiomsTheory.

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

Fixing typos in the documentation (included as a comment in sexp.sml).


The method of converting a full ACL2 name pkg::sym to a HOL-friendly
name is as follows (see definition of create_hol_name below).

1. First see if the ACL2 name already has a HOL name, and if so
return it.

2. Convert sym to a HOL name, say hol_sym, using the ML function
acl2_name_to_hol_name (this function is described below).

3. Check to see if sym_name is already used. If not it is the result.

4. If hol_sym is in use, then use acl2_name_to_hol_name to convert pkg to
hol_pkg and then see if (hol_pkg ^ "_" ^ hol_sym) is used, and if
not return it. If it is used an error report is printed and an
exception raised.

5. Record any names generated by step 1-4 above in acl2_names.

The function acl2_name_to_hol_name converts a string s to a
HOL-friendly name as follows.

1. Convert s to a list of characters and convert all letters
to lower-case.

2. Replace "-" by "_".

3. Replace special characters by strings of letter characters
using acl2_to_hol_char_map (defined below). Add an underscore
"_" to separate special characters from all other characters.

We think these simple rules should be sufficient in practice, and if
they are not it's better to reconsider carefully what to do rather
than to have ugly looking names generated by more complicated rules
(this might change if the sufficiency assumption is badly wrong).

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

Various updates, including stuff for importing ACL2 theorems.

Added support for papallel lets in HOL to correspond to lets in ACL2.

Tidying up.

Various updates + filter-forms.csh from Matt (see:
http://www.cl.cam.ac.uk/~mjcg/hol2acl2/backpack/GordonHuntKaufmannPaper.html)

Missing "COMMON-LISP::" package name when printing "COMPLEX"
(spotted by Matt Kaufmann).

----------------------------------------------------------------------
----------------------------------------------------------------------

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