Move some term-equality helper functions from boolLib to boolSyntax

This helps with dependency chains and provides some documentation in
that they now appear in a signature file for the first time.

Store "local" theorems (e.g., with Triviality) in DB

The reverse lookup now returns the list of "locations" where a theorem
is available.

Implement, document and regression-test some "term tactics"

Move DefnBase to src/coretypes, make progress with one_line_ify

DefnBase is now home to the updated literal-decider conversion

Allow theorems to be stored "locally", with local attributes

Such theorems are not stored in the exported theory, but do
temporarily affect the global contexts that their attributes point at.

The test-case illustrates this, with a local simp not visible in the
later theory.

Move theorem-attribute "parser" implementation to ThmAttribute.sml

Rework ThmSetData implementation to use Theory s-expressions

This makes the encoding more robust, particularly if set "removal
instructions" might include space characters.

Correct spelling mistake in comment

Refactor handling of thm attributes ("simp", etc) into new module

A slight backwards incompatibility is that this removes the ability
for script files to declare new attributes (hence removal of
attr[12]Script.sml from src/1/theory_tests). This facility is used
vacuously in CakeML once.

Rework persistent ThmSetData API to allow for "removal" of elements

The removals are strings encoding removal "instructions", which are up
to the underlying consumer to interpret. Still to test any of this
new machinery, but the old behaviours have been preserved.

Rationalise eq fns in boolLib to have _eq suffix

Exception is Teq and Feq, which are not eq functions (binary
relations), but are actually unary predicates on terms.

Actually get boolLib to compile (!)

Reorganise term-equality functions in boolLib

Useful functions for dealing with terms up-to aconv

Taken from remove-term-eqtype branch

Remove TABs in some source code, replacing them with spaces

Use Emacs's conception of how many spaces the TAB was
representing (and the M-x untabify command).

This may not line up with the author's original conception, but then,
using TABs makes it impossible to tell just what the original
conception was in the first place anyway.

Should probably script this over all of repository (excluding
makefiles of course), and use standard expand or col utilities rather
than emacs.

Remove eqtype declaration for term type

Move variant_of_term to boolLib from pairTools

This makes it visible (previously pairTools did not export it).

Utility to extract sub-terms where inputs differ

ThmSetData passes thms *and* names to consumers

The names were always available, but the API now changes so that
consumers get names as well as theorem values. They can ignore the
names of course. (In this context, consumers are things like the
stateful rewriter, the monotonicity rule database, the TFL congruence
rule database etc.)

This will be helpful in allowing the stateful simpset to know what its
theorems are called, which is progress with Github issue #313 (to allow
easy removal of rewrites from a call to the simplifier).

Isolate some parsing within boolLib.sml

It's possible to get a (perhaps only Moscow ML) build to clash with
the code here if there are theories around that make constants of
names like "f" and "g".

Implement new scheme to allow simple addition of theorems to theorem "sets".

When saving or storing theorems, simply add [name1,name2] strings to the
end of the binding, and the theorem being saved will be added to the
theorem set with that name.

Remove trailing whitespace in source files.

Change src/bool to src/1 as a prelude to experimentation!