Again allow ancestral data to consume deltas all at once on theory-load

This allows named simpset-fragments to be added to srw_ss. This then
allows those fragments to be easily removed with calls to
diminish_srw_ss. In the 'fix-ancestry' rework this ability was
removed but this did break proofs when diminish_srw_ss calls had no
effect.

Selftest in coretypes demonstrates this with removal of the "one"
fragment.

Provide more ancestry-based entrypoints for stateful simpsets

In particular, allow for recreation of the simpset as it existed on
theory entry. E.g., a call to

recreate_sset_at_parentage (parents "list")

will make the simpset take on its value as it existed when execution
of the listScript began.

Make global simpset state easier to recreate with "logged_update"

This entry-point records that a change to the global simpset has
happened within a piece of code (rather than a script). The change is
made (as before), but the change is also recorded so that it can be
recreated/applied to different base simpsets.

Make TypeBase ancestry-aware

The fix to Boolify/src/Encode.sml attempts to be semantics-preserving,
but there are no test-cases for this code.

Extend BasicProvers interface with temp_setsimpset

Reimplement global simpset to be "ancestry-aware"

Allows API to be enriched with {temp_,}set_simpset_ancestry and
thy_simpset functions.

Both of these don't fold in appropriate additions from the TypeBase
after these calculations yet.

Tweak ThmSetData API: take callbacks with more honest types

In particular, the callbacks are always only ever called on singleton
lists, so it seems silly to ask the user for functions with types that
have lists.

Simplify handling of diminish_srw_ss by forcing it to initialise

The whole behaviour whereby srw_ss waits to "initialise" itself now
smells a little of being a premature optimisation to me.

Move some of the machinery behind BasicProvers.VAR_EQ_TAC to Tactic

Fix diminish_srw_ss invalidating earlier call to temp_delsimps

With test cases. Also change type of simpLib.remove_ssfrags to have
the acted on type and return type be adjacent. I.e., prefer

foo : B -> A -> A

over

foo : A -> B -> A

as the former curries to create a nice update function.

Alter VAR_EQ_TAC to call TIDY_ABBREVS after invocation

TIDY_ABBREVS "purges" abbreviations that have become malformed, where

- "malformed" means no longer of form Abbrev (var = exp), with exp not
itself a variable
- "purge" means Abbrev(e1 = e2) becomes e2 = e1, and Abbrev(other_exp)
becomes other_exp.

The action of TIDY_ABBREVS is included in the ABBREV_ss simpset
fragment, which is in turn included in the stateful simpset.

The calling of TIDY_ABBREVS is the only change in the behaviour of
VAR_EQ_TAC, and this can be turned off with the
BasicProvers.var_eq_old trace.

Attempt at better Abbrev protection

This in the face of simplification and the variable elimination done
by RW_TAC and friends. Core sequence, -t1 and some of -t2 builds (up
to category theory example).

Machinery for dynamically reverting to the old behaviours possible
through diminish_srw_ss and a trace variable.

This is work on github issue #800

Update src for strip_binop change

Allow Induct_on & Cases_on to use different theorems with 'using'

The using function is infix on tactics; other tactics can grab 'using'
theorems if they want to try, using the markerLib.maybe_using
entrypoint.

Ensure diminish_srw_ss removes builtin ssfrags before initialisation

Otherwise, you had to put the diminish_srw_ss call after srw_ss had
been "initialised".

With a test case.

Reinstate a way to refer to labelled assumptions

This got lost in c76376ed3f7d (2008!).

It clearly isn't being used, but I may want it in the near future.
Change the name from LB to L. With markerLib open, one can write
things like

simp[L"mylabel",...]

to get access to the assumption labelled "mylabel".

Also, using a congruence, stop the stateful simpset from rewriting
under labels.

Provide new term-based version of Cases_on

This version takes an extra string list parameter for specifying names
to be used in the split.

add boolSimps.NORMEQ_ss to stateful simpset

Change "thm-names" (used in various places) to be Thy-Name record

This saves on pulling things apart and looking for dots and the like.
It changes the simpLib API (most significantly for the SSFRAG function
which builds simpset fragments).

Remove non-exhaustive match warning

revised namedCases{_on} to support auto-name generation for underscored names

adding ability to specify names introduced by Cases and Cases_on

Tidy up some src directories for line-lengths

Tweak Induct{,_on} to be more robust wrt baddly behaved thms/tactics

In particular, fall back on a HO_MATCH_MP_TAC call as a last resort.

Complete implementation of smarter Induct_on

This massages a goal to pull out a negative occurrence of a inductive
relation term, replacing compound terms with variables and
generalising appropriately to make the goal suitable for a subsequent
call to ho_match_mp_tac (which is done inside Induct_on).

Not sure yet quite what should be done with mutually recursive
relations and Induct_on.

Closes #244

Implement Req0/ReqD forms to require simp rules to have been applied

Closes #680

Provide entry-point to temporarily remove rewrites from srw_ss

So, delsimps ["foo", "bar", "baz"] removes those rewrites and exports
the change to future theories; temp_delsimps ["foo", "bar", "baz"]
removes the rewrites temporarily (i.e., only in the current theory).

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.

Make sure that rewrites are exported with names

This means that most theorems in a simpset will have names that can
then be the basis for rewrite removal.

Give theorems names in simpsets

This is to allow them to be removed easily. System builds on -t1, but
there are still two things to be done

1. the names associated with export_rewrites calls aren't passed on to
the simpsets yet
2. there is not yet an API for removing them

Also, perhaps just as an interim measure, I removed the unused
entrypoint for removing rewrites by pattern matching against their
LHSes (simpLib.remove_theorems).

Move without loss of generality tacticals to new library.

Add “SPLICE_CONJ_CONV”; add tacticals “wlog_tac” and “wlog_then”.

Remove eqtype declaration for term type

Remove an unnecessary ref in BasicProvers.sml

It looks to me like this was coded using a reference (in
fe8b6c9c40bb6c0d2a9a185c5a7bc6f0934b23ee) just to be able to use app
rather than foldl. The app, in turn, was there from PolyHash days.

Prompted by, but does not solve, #477.

Remove some stale redeclarations of things like THEN1 and >-

Similarly, remove some unnecessary infix declarations for the same
tokens.

Finally, rename an internal variant of THEN1 used inside BasicProvers
so as to make it clearer that it is an intended variant.

Make by and suffices_by report failing tactics with line number

Include test cases

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

Progress with github issue #407

Refactor more parsing code

Aim is to move more specialised functions out of Parse and make clients
use TermParse. Here, the functions in question are those to do with
"parsing in context", where a context is a list of free variables to
treat as constants, and an optional type constraint.

In the change to BasicProvers, this allows a constraint that the
argument to "by" be boolean to be introduced.

Get BasicProvers to compile

More moving lcsymtacs implementations elsewhere

Eventually lcsymtacs will just be a bunch of 'open' declarations, and
then people won't bother to include it at all.

Make type explicit to help mosml compilation

It can't handle

map #2 thms

if the type of thms isn't explicit at the function level.

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

BasicProvers ind'n tacs more uniform on datatypes and "non-datatypes"

Includes test-case of sorts.

Make "by" quieter when the provided quotation doesn't type check.

Also make sure that a typecheck error message exactly coincides with the
corresponding exception's message.

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.

Correct typo in comment

Improve the speed of EVERY_CASE_TAC

It was adding a bunch of datatype theorems each time through the loop,
which was expensive on developments that contain large datatypes. Now
it builds them into a simpset at the start.

Implement new suffices_by tactic in BasicProvers and bossLib.

Closes #116.

Fixed case-splitting tactic in BasicProvers.

Problem, inevitably, was that the code thought the examined term was
last, but now it’s first.

Adjust (and reduce) interface to ThmSetData.

The change is to add an extra string parameter to the callback
function that the client provides. This is the name of the theory
which has stored the theorems. This change prompted the changes to
computeLib, IndDefLib and DefnBase.

The reduction was to remove the ThmSetData's new function, forcing
BasicProvers to use new_exporter. This was possible because of the
extra information provided to its call-back.

I also wrote some test-cases mimicking the original problem that
Magnus and Ramana had, and prettied the warning output.

This closes #73.

Rework various Theory hooks into one general framework.

The basis for the framework is the TheoryDelta type. Client code can
ask to be notified of theory changes, and will have their provided
call-back function called at appropriate times.

This commit hasn't adjusted the theory functions for
{add,del}{const/typeOp} yet; it has just unified the existing
functionality (register_onload, after_new_theory and
register_onexport).

Delete trailing whitespace throughout src/

Added once, modified, committed, pushed.
Now re-add, recommit, repush. Sheesh.

Improvements to Induct and Induct_on for non-datatypes.

Remove trailing whitespace in source files.

Improved EVERY_CASE_TAC.

Removed Lib.gather. Use {Lib,List}.filter instead.

Final minor fix to FULL_CASE_TAC and EVERY_CASE_TAC:
don't use SIMP_CONV bool_ss ... in the assumptions,
since it can "over-rewrite" the assums, e.g.,
changing the IH so that later proof steps don't
work.

Bug in TypeBase.is_case. It would return true
on

option_case NONE

Fixes to CASE_TAC to make proofs in Boolify go through.

Fix to CASE_TAC, which could loop on nested cases over the option type
(and thus, presumably other types as well). Also, added a few more
entrypoints for case-splitting, e.g. FULL_CASE_TAC (do a case split
anywhere in goal, including assumptions) and EVERY_CASE_TAC (do all
possible case splits).

Also beefed up NORM_TAC so that it splits case expressions. Possibly
this could be migrated to RW_TAC and kin, but that might break a lot
of proofs.

Put my Induct_on functionality back into BasicProvers.sml

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 a few more operations for working with simpsets and simpset fragments.
In particular, added the facility to remove named fragments from a simpset.
This is done fairly crudely -- the new simpset is simply rebuilt using all of
the remaining fragments.

This enables you do do things like:

- SIMP_CONV (simpLib.remove_ssfrags (srw_ss()) ["word arith"]) [] ``...``

and

- val ss = diminish_srw_ss ["word arith","word logic"];
- e (SRW_TAC [] []);
- val _ = augment_srw_ss ss;

Doing this will re-order the fragments, which I believe can affect behaviour?
diminish_srw_ss isn't persistent -- not sure if that is good or not.

The new operations are:

> val name_ss : string -> ssfrag -> ssfrag

(* Give a name to a fragment. *)

> val named_merge_ss : string -> ssfrag list -> ssfrag

(* A version of merge_ss that allows users to name the merged fragment. *)

> val std_conv_ss : stdconvdata -> ssfrag

where

type stdconvdata = { name: string, pats: term list, conv: conv }

(* A simplified interface to conv_ss. For conversions with: no
side-conditions, trace level 2 and for a list of "variable only" keys. *)

> partition_ssfrags : string list -> ssfrag list ->
(ssfrag list * ssfrag list)

(* Partition a simpset fragment list: lhs for fragments in a list of
names and rhs for those not in the list. *)

> remove_ssfrags : simpset -> string list -> simpset

(* Remove named fragments from a simpset. *)

> diminish_srw_ss : string list -> simpLib.ssfrag list

(* Remove named fragments from srw_ss. Returns removed fragments. *)

Slightly polish ThmSetData, and start to use it in lambda example.

Revise LoadableThyData implementation to be a bit cleaner in what it
requires of clients. Documentation still to come.

Complete implementation of generic theory data feature, and use it to
implement the exportable rewrites used in srw_ss(). The code still
needs some more polishing. Hopefully that will come as I convert
other "stored data features" to use the same underlying code.

Make the Once and Ntimes functions work properly with the
simplification tactics here by eta-expanding so that the insertion of
the modified rewriting theorem only happens when there is a goal to be
acted on.

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.

Additional functionality for abbreviations.

1. The labels library has been merged into
markerLib and the src/labels directory eliminated.
2. Have added markerSyntax structure.
3. Operations on abbrevs used to all be in
structure Q, even those that didn't deal
with quotations (like UNABBREV_ALL_TAC). Now
markerLib provides all abbrev. operations and
these take terms. Operations that benefit from
quotes, e.g., ABBREV_TAC, MATCH_ABBREV_TAC, etc.
are still to be found in Q.
4. Abbrevs are kept reduced by the simplifiers and
there is a REABBREV_TAC which can be separately called.
This sorts abbrevs topologically, so that they get
restored in a sensible order.
5. For situations where one wants to get rid of all
abbrevs, apply a tactic, and then restore the abbrevs,
there is WITHOUT_ABBREVS: tactic->tactic.
6. Have added a simple topological sort to Lib.
7. Updated proofs in the src directories, and also
in examples/lambda.

Having FULL_SIMP_TAC there broke proofs too - taking it out for the
moment.

REABBREV_TAC is wrong because it doesn't necessarily re-abbreviate in
the right order (messing up proof states). To get a reasonable
approximation of what reabbrev is trying to do, FULL_SIMP_TAC with the
pure simpset will apply the abbreviated rewrite (var = rhs) the "other
way round".

Changed behaviour of simplifier to
propagate the abbreviation coming from
a let binding in the goal being moved to
the assumptions. This helps keep the goal
in "fully abbreviated form". Also added

Q.REABBREV_TAC

which re-abbreviates the goal and

Q.WITHOUT_ABBREVS tac

which temporarily removes all abbreviations,
runs tac, then reabbreviates.

Probably, Q is not the right place for these
functions, but the rest of the abbreviation
stuff is there.

Also added some internal documentation on what
Q.ABBRS_THEN does, and the like.

Remove another instance of Polyhash from the sources.

This check-in mainly fixes a problem with
literals occurring in patterns of TFL-style
definitions. There are a host of other minor
changes as well.

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

Committing in revision of incorporation of 'literal_case' into
automatic simplifiers.

Before, only SRW_TAC automatically simplified occurrences of the
'literal_case' constant. Now it is built into BOOL_ss, as well as
being available separately as literal_case_ss. This means that
most normal users will never have to deal with 'literal_case' if
they use a simplifier.

Modified Files:
hol98/src/basicProof/BasicProvers.sml
hol98/src/simp/src/boolSimps.sml
----------------------------------------------------------------------

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

Committing in fix to SRW_TAC so that it can solve elementary case
expressions, such as (case 1w of 1w -> x || _ -> y) = x.
Bug discovered by Anthony Fox.

Also commiting in extensions to quotient library to better support
the new constant 'literal_case'.

Modified Files:
hol98/src/HolCheck/stringBinTree.sml
hol98/src/basicProof/BasicProvers.sml
hol98/src/quotient/src/quotient.sml
hol98/src/quotient/src/quotientScript.sml
hol98/src/simp/src/boolSimps.sig
hol98/src/simp/src/boolSimps.sml
----------------------------------------------------------------------

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

Committing in possible fix for bug in SRW_TAC dealing with the new
literal patterns. Bug found by Anthony Fox.

Modified Files:
BasicProvers.sml
----------------------------------------------------------------------

Upgrading Define so that it proves more termination goals.
Generates lex. combinations and tries them out, so gets
some more ordinary recursions. Gets all iterated primitive
recursions. Also has been taught about some operations
on words (so recursion from w to w-1w will terminate,
for example).

Let me know of any bugs/slowdowns, etc.

Changed the TypeBase to be indexed by types. Originally it was
indexed by a single string (representing the type operator), then
Michael changed it to a pair of strings (precise representation
of the type operator). The latest change allows non-datatypes to
be added to the TypeBase. This will allow case analysis and
termination proofs to be supported for non-datatypes.

I reckon there are still a few bugs left after the massive
revision, so you might want to wait a while before upgrading.

Changed a couple of misleading/annoying names. The type ssdata is now
called ssfrag (to bring it into line with documentation that talks about
simpset fragments), and the constructor SIMPSET is now called SSFRAG.
It never created a simpset, so the latter was a stupid name.

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

The implementation of Abbr has moved to markerLib.

Make LET_ELIM_TAC part of STP_TAC, and thus SRW_TAC and RW_TAC.
The LEAVE_LET theorem can be used to tell this not to happen if included
in the list of theorems passed to the rewrite tactics.

New entry point in BasicProvers called LET_ELIM_TAC to do lovely things
with lets, whether uncurried or not. They're lifted out of the goal
and turned into abbreviations into the assumptions. Plan is to tack
LET_ELIM_TAC into the basic action of RW_TAC and SRW_TAC as well.

New treatment of abbreviations. Documentation still to be updated.
Backwards compatibility illustrated in examples/lambda/standardisationScript
and examples/arm6. New techniques and entry-points illustrated in
core distribution and some of the lambda example scripts.

Sorry! I've realised that there's a better way of doing what I want
within the netsem code-base, and that I don't need to make any changes
to the way HOL currently does things. More, that letting HOL stay
just the way it was is probably better. So, this change is to put the
code I meddled with over the last couple of days back the way it was
originally. (Minor exceptions include changes to comments, elimination
of unnecessary infix declarations, and revealing a PAIR0_ss that is
equal to PAIR_ss minus LET_ss.)

Fixes for a couple of infelicities:

* bool_ss didn't ever treat LETs (why?), so my incompatibility blurb wasn't
accurate. I had messed with the behaviour of PAIR_ss though, and this
was unnecessary. The new arrangement of things changes only the
behaviour of the srw_ss.

* Yesterday's solution for computing with lets would allow a subsitutiion
to occur even before the argument to the let had been simplified.
The new scheme uses a congruence rule to evaluate the sub-expressions,
and after doing so, wraps the value in an I tag. Then the various
LET_{foo,bar,baz} theorems can fire and cause a substitution to occur.
The presence of the I encodes "I have been looked at by the simplifier".

I want this because I want to have tags that indicate likely "value-hood"
such that a whole expression can be substituted at once, but I don't
want to not get a chance to simplify that expression first. Imagine,
for example, that NUMERAL could occasionally occur wrapped around
expressions that weren't already values. Then the theorem
|- LET f (NUMERAL x) = f (NUMERAL x)
would cause the pending computation x to be distributed willy-nilly
around the body of f, potentially causing us to have to simplify it
multiple times.

In the new scheme, the theorem above isn't used. Instead we have
|- LET f (I (NUMERAL x)) = f (NUMERAL x)
and by requiring the presence of the I, the reduction won't happen
until the simplifier has looked at x. Now, this shouldn't happen with
numerals, but it might well happen with other tags I'm planning to use.

So there you go.

Fix minor formatting infelicity.

Minor fixes to support rewriting annotations.

Us HOL_PROGRESS_MESG to allow me to get an idea how long this srw_ss
initialisation is taking. (Useful for very big TypeBase's, as happens
in Netsem.)

Don't export rewrites unless there are rewrites to export. (As it stands,
every theory was getting a thy_rwts binding in its signature bound to
a probably empty ssdata.)

Modify export_rewrites to allow for multiple calls to this function
within a session. This makes it easier to ensure theorems are exported;
they can have this done at point of proof, rather than needing to be
gathered together at the end of the file. The idiom for getting this
done is based on the way grm_updates is handled in Parse.sml (an idea of
Konrad's); note the funky use of a reference variable within a closure's
environment.

Modify TypeBases so that they can store conversions as well as theorems
in a tyinfo's "simpls_of" slot. This is then used to implement a conversion
for enumerated type equalities. Previously, we just used a rewrite
directly, which meant that something of the form (x = C10) might turn
into the rather ugly (foo_to_num x = 11). Now, the rewrite is only
applied to equalities between constants.
Some comments in the .sig files in Datatype, RecordType and EnumType
hopefully also make it clearer what the weird string results are
doing, and how they get added into theory files.

A couple of additions to the stateful rewriter: I got thoroughly sick of
having to write combinTheory.o_THM, and was also surprised to see that
FILTER P (h::t) wasn't being dealt with automatically (though it does
introduce a case-split).

This fixes a pretty obscure bug:

g `(h::t = x::y) /\ (SUC z = SUC w) ==> P x y`;
e (BasicProvers.PRIM_STP_TAC boolSimps.bool_ss NO_TAC);

goes into an infinite loop. The reason is that after simplification, the
goal looks like

P x y
----------
0. h::t = x::y
1. SUC z = SUC w

The code for PRIM_STP_TAC then sucks those assumptions that are equations
between constructors off the list and puts them back on after simplifying
with the simpset (bool_ss in this case). Because bool_ss doesn't affect
either, they are put back unchanged, but in the wrong order. The controlling
logic in PRIM_STP_TAC repeats this process under a CHANGED_TAC.

Arguably the fault lies in the logic that assumes the given simpset will
always be able to modify (for the better) equations between constructors, but
fixing this seems harder. Instead, my fix just makes sure that the relevant
assumptions get put back on in the right order.

Changed the type (and nature) of register_update_fn in TypeBase.

Before, you registered a function that got to see a tyinfo before it
was added to the TypeBase. All well and good.

Now, you register a function that gets to modify a list of tyinfos
before they're added to the TypeBase. Distinctly hairier.

Why allow changes? Well, how else can I register a piece of code to
add "boolify" entries to the tyinfos.

Why a list of tyinfos, instead of one at a time? Well, with mutually
recursive datatypes, you really need to see all of the tyinfos at the
same time.

Note that now the order of execution of these update functions is
significant. They get executed in the order that they're registered,
so something registered after boolification gets to see the "boolify"
entries and make use of them.

This additional explicit dependency can help stop Holmake getting confused.

Initial ideas towards labelled assumption implementation.

Minor changes to STP_TAC.

Added VAR_EQ_TAC to BasicProvers. It eliminates assumptions of the
form v = M or M = v (provided v doesn't occur as a proper subterm of M).

The other changes are just messing about.

Missed one occurrence of PolyHash. W2K wins again.

Minor changes.

Replaced 4 occurrences of 'PolyHash' with 'Polyhash'.

How did this ever work?

Simplified some proofs in MachineTransitionScript.

Reverted to Taupo-6 RW_TAC. This should make RW_TAC faster, and a little
less eager to case-split conditionals. Some proofs may break as a result.
In that case, use the drop-in replacement BasicProvers.NORM_TAC.

Term destructors now operate using same_const to check the operator
of the term being destructed. This may increase efficiency somewhat.
There were consequent changes to the xSyntax modules of the system.

More machinery to make the "stateful" rewriter even snappier.
Script files for theories can now do a
val _ = export_rewrites ["th1", "th2"]
where the argument is a list of strings corresponding to theorem names.
If the theorem names are from the current theory, they can be quoted
as is. If theorems are to be included from elsewhere, dotted IDs
have to be used.

When the corresponding theory loads, it automatically extends the
stateful rewriter's underlying simpset with the given simpset. The
theory's interface is also extended with a value thyname_rwts of
type simpLib.ssdata corresponding to the rewrites specified.

Modified so that the work involved in constructing the srw simpset doesn't
take place until the simpset value is requested via get_srw_ss, or the
tactic SRW_TAC is called. (The "work involved" can be quite substantial,
and if this tactic is not going to be used, it is unfair to force it on
users.)

Minor fix to STP_TAC. Doesn't make it go any faster.

Change stemming from split of TypeBase into TypeBasePure and TypeBase.

New SRW_TAC tactic (stateful RW_TAC) implemented.

Modifications caused by change of TypeBase signature.

Minor changes.

Minor change.

Changes to basic STP_TAC for rewriting/simplification. Junk like
T, F will no longer appear on assumption list. Also, case splitting
on if-then-else is smarter in cases of nested ifs in the test. Also,
boolean variables on the assumptions (or negated such things) get turned
into var-equalities and blown away.

Kananaskis compatibility.

Minor changes to accomodate change to simp/src/boolSimps (I think).

Split-off from bossLib, so that these things are available earlier
in the development of the system.