Remove TABs from src

Will also make selftest to check that they aren't introduced

Fixes of bag, container, finite_map and in n-bit/

Get core HOL to build with new definition of "by"

Progress with github issue #407

Remove unnecessary structure bracketting

As per 89fc99bc3, but on as many examples as a grep -R can find.

Clean src/ to remove Unicode (or to mark it as OK)

Marking Unicode as OK is done by putting the UOK tag on the same line of
the relevant file.

multiset order specialized to worklist algorithms

removed extraneous parens, also irule IMP_ANTISYM_AX -> EQ_TAC

alternative definition of LIST_TO_BAG, lemmas, shorter proofs

src/num/theories/SingleStep.{sig,sml} is gone. The
defininitions of Cases, Cases_on, Induct, Induct_on,
CASE_TAC (and co.) are now in basicProof/BasicProvers.
completeInduct_on and measureInduct_on are now in
numLib. recInduct is now in src/tfl/Induction.sml.
All these are collected in bossLib, so the changes
should be invisible to ordinary users.

SingleStep.*.doc has been changed accordingly.

BasicProvers.NORM_TAC should now automatically perform
all case splits (from if-then-else expressions as
well as case expression) arising anywhere in the goal.

Added theorem to containerTheory relating LIST_ELEM_COUNT to LIST_TO_BAG.

Added CARD_LIST_TO_BAG to containerTheory, as a rewrite.
Also removed the Unicode from the last checkin.

Added BAG_TO_LIST_EQ_NIL to containerTheory, and made it a rewrite.

removed utf-8 from my last commit

some theorems about LIST_TO_BAG and LIST_TO_SET

Make LIST_TO_BAG_def an automatic rewrite and rename its internal uses
to reflect its external name.

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!

BAG_EVERY, BAG_ALL_DISTINCT and BAG_OF_FMAP were introduced. There are theorems about the new definitions. Moreover there are mixed theorems about existing functions, most noticeably about LIST_TO_BAG.

Change export_rewrites back to its old API (without requiring an extra
string). When exported, the resulting simpset fragment always picked
up the name of the theory to be the base of its name, so there didn't
seem much point in giving users a false impression of naming power.

A whole mess of small changes intended
at making simpsets prettyprint informatively
in the interactive loop. Very possibly
I haven't updated all the files in the examples
directories.

Move pred_set to be earlier in the build sequence, making it an
ancestor of listTheory, and available in bossLib. The various
LIST_TO_SET and SET_TO_LIST theorems are now available in listTheory.
Also introduce the set abbreviation for LIST_TO_SET that I've found
very useful. Documented in release notes as an incompatibility.
Incidentally reckon containerTheory might be something we could do
away with entirely.

Add a new exported rewrite to pred_set, and use it to prove another
export-worthy rewrite in the theory of containers, namely that
SET_TO_LIST {x} = [x]

Follow-on fixes to changing Term to Parse.Term and Type to Parse.Type
in the quotation pre-processor. A mass of trivial changes, but the
new way of dealing with files containing code that does parsing
(not script files) is to

* grab the ambient grammar(s)
* set the current grammar(s) to the right values
for parsing quotations in the file
* the body of the file
* reset the current grammar to the ambient grammar

For an example, see src/taut/tautLib.sml

ML code generation for finite_map now added. Also, a whole host
of minor changes and robustifications have been applied.

I'm harder pressed to explain why I prefer this new theorem
as the rewrite compared to the version the other way round.
Gut instinct or something. I'm not super-convinced so if you
reckon I've got it wrong, speak out and I can drop it.

Forgot this one.

Move LIST_TO_SET into listTheory from containerTheory as part of my general
campaign to move set "things" as early as possible into the build sequence.
Also add various theorems about lists and bags.

Minor inconsequential cosmetic changes made in the course of tracking
down various bugs.

Additional theorems in containerTheory.

Added support for recursive definitions on finite bags. Added the
theory "container", which is meant to relate all the container-like
datastructures in the system (sets, bags, lists, and maybe finite maps).