Some more additions to bagLib. I'm mainly interested in bags that consists of multiple insertions into the empty bag like for example {|x1;x2;x3|}.
I call these explicitly given, finite bags "simple".

There was a lot of tool support for handling bags that consists of BAG_UNION applications. One can eliminate those for example on both sides of an equation, a BAG_DIFF ...
Now I added support for these "simple" bags. I started adding some things like resorting to bagLib before. However, these addidtion became larger and larger. Therefore, I moved them
into an new file called bagSimpleLib. However, it is imported by bagLib, so the end-user does not need to know this.

Fixed a bug. Previously it did not compile with mosml due to dependeny error that were masked in Polyml.

BAG_IMAGE_CONV added that is able to evaluate BAG_IMAGE on very simple bags. Moreover, some extensions to bagSyntax were made.

Was failing to build under Moscow ML.

Compiling bagLib.sig
Compiling bagLib.sml
File "bagLib.sml", line 30, characters 46-50:
! fun BAG_RESORT___BRING_TO_FRONT_CONV 0 b = REFL b
! ^^^^
! Unbound value identifier: REFL
Build failed in directory /Users/acjf3/HOL/src/bag

Added BAG_RESORT_CONV. This new conversion is able to sort nested uses of BAG_INSERT. For example
BAG_RESORT_CONV [0,3,2] ``{|x0; x1; x2; x3; x4|}`` results in {|x0; x3; x2; x1; x4|}

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!

Slight re-org.

Builds in Kan.0.

Kananaskis compatibility.

Minor fix to SBAG_SOLVE. It's possible that part of the context will be
facts about bags over completely different types. It's pointless trying
to SPEC these with the variable chosen of the base_type of the goal.
We use mapfilter to retain only those assumptions that can be so SPECed.

CANCEL_CONV can loop where both arguments to the binary function are
the empty bag. This can't be allowed in a simpset, so the actual conv
used in BAG_ss is now CHANGED_CONV CANCEL_CONV.

Extended bag library. Decision procedure for solving sub-bag or
equality goals has been added. The CANCEL_CONV conversion has also
been extended to do its thing over BAG_DIFF terms. It has been put
into BAG_ss. If it proves to be too inefficient there, I can always
take it back out.

Implemented a bag library, to help with standard tasks, and provide at
least one useful tool (CANCEL_CONV).