Allow Unicode lambda (λ, U+03BB) in src/

This is because writing things like (\(x,y). x + y) puts editor modes
into strange states when they think the second left-parenthesis has
been "escaped". Allowing a lambda to be used here gives us a chance to
avoid confusing editors, and who wouldn't want that?

Make parsing fail if Unicode logical negation (¬) applied to numbers

With test cases.

Closes #753

Prove a version of EXISTS_UNIQUE_ALT in boolScript.sml

There is an EXISTS_UNIQUE_ALT proved in boolLib; this moves a version
to the DB (match and find will see it) called EXISTS_UNIQUE_ALT'. It
flips the direction of the equality on the RHS, so that rewriting a
?!x. P x in the assumptions will give a new assumption (after
stripping) that looks like

!y. P y <=> (y = x)

My theory is that this direction (y = x) will be more useful as an
elimination. (And if not, use the original EXISTS_UNIQUE_ALT.)

Make equality of "tight" precedence by default

Start to work through knock-on effects of this.

Add DISJ_EQ_IMP to boolTheory

Prove {FORALL,EXISTS}_itself

Simplifying with EXISTS_UNIQUE will give this effect pretty directly,
so this is more an exercise in proving stuff in boolScript than
anything else.

Fix bug in generation of case_eq theorem for 'a itself

Remove TABs from src

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

Record width=3 for standard TeX iff (⇔), which is suprisingly huge

Remove some early code assuming term is an equality type

Use Unicode quotes (“...”) rather than --` ... `-- and ``...``

Need to do this in boolScript felt particularly pressing given the --
syntax. This is a horrible holdover, and consumes many columns
(particularly when the frequently required parentheses are also
included).

I think there are relatively simple regular expressions for doing this
automatically. For the moment, bool and arithmetic are two
trailblazers.

Get hol.bare to compile/build

let-rules not handled correctly by Absyn

WIP for change to list syntax handling.

Very broken at the moment

Move absyn post-processing done for let-expressions to boolpp

This removes this behaviour from the core-parser, which is a win for
simplicity, and makes it use the same (standard) API as other
absyn-postprocessors (such as those used to implement monad syntax).

This modularisation is a step towards making the let-syntax richer (as
per github issue #154, which calls for Isabelle-style syntax).

Extract pretty-printing of LET-terms from term_pp.sml

It is now part of user-printer "land" in src/bool/boolpp.sml,
alongside the custom printer for if-then-else (COND).

This refactoring revealed a bug in the way overloaded constants
couldn't be handled by user-printers if they could have extra
arguments hanging off to the right (as in “LET f x y”), *unless* they
were overloaded to "case" (as in COND).

To make sure one's user-printer is going to work, you have to consult
the grammar's overload information to check if your term is one you
want to print according to the grammar_name function. Unfortunately,
looking for particular constants is not guaranteed to work, as the
process of descending terms in the pretty-printer is liable to turn
real constants into special "fake" constants that are actually
variables with special names.

This is progress with Github issue #154, to allow new (Isabelle-style)
syntax for let expressions.

Preserve add_user_printer properly in grammar data

This requires a slightly involved process for storing references to
code in theory files.

Update the .doc file on add_user_printer (which was already incredibly
long), and add a test.

Closes #367

Properly enable case-expr p/printing overloads

This had been made the responsibility of the process that stored
TypeBase information, but that didn't interact properly with the
user-delta approach to storing grammar changes. Now the persistent
overloads are emitted separately.

Fix one of the bugs in previous commit's test-case

This was done by simply removing the entry-points (uoverload_on, and
uset_fixity) that were causing problems. They have long been redundant
in terms of their desired effect, and introduced buggy behaviour with
the switch to explicit grammar deltas.

The uoverload_on function is still used internally.

Remove redundant calls to add_const in boolScript

Remove redundant add_type calls

boolSyntax.new_type_definition called add_type after a type was defined,
even though the hook machinery now takes care of this.

In boolScript, there was a similarly unnecessary call to add_type after
the itself type operator was defined.

Remove unnecessary structure bracketting

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

Generalise type in boolTheory.literal_case_RAND.

Remove uses of OpenTheoryMap from boolScript.sml

Eventually OpenTheoryMap is probably going to be deleted entirely.

Allow multiple case-like constants in a grammar

Parsing handled; printing still not quite right

patternMatches turns on pmatch, adds .| infix

Eliminate some instances of "val _ = save_thm".

OpenTheory names for ind, ONE_ONE, and ONTO

Revert "start experimental implementation of revised new_specification"

This reverts commits 7f58ad8, eae01bc, and c07a105.

replace calls to new_specification in boolScript.sml

rename OpenTheory name for bool$IN, to match current stdlib

Start of project to flip argument order in case constants.

One scary (but probably optional) change is to do away with bool_case
constant because it is now identical to COND. This could be reversed,
but having two constants with exactly the same type and semantics does
seem silly. I think the parsing/pretty-printing behaviour can be made
sensible even in the face of this unification.

Prim_rec’s functions for defining case constants and proving case
congruence theorems have been adjusted appropriately.

This is relevant to Github issue #97.

fix OpenTheory name for min$@

Apparently it has moved out of the Data.Bool namespace in the standard
library. (The library is not really standardised yet :))

Try to clean up some more proofs in boolScript.

Most of this work makes the SML cleaner without making any difference
to the actual proofs.

Simplify proofs of PULL_{FORALL,EXISTS} theorems in bool.

These are instances of already proved facts (that have confusing
orientations and confusing names). The PULL_ name is definitely an
improvement here.

Also define and use a LIST_CONJ helper throughout all of boolScript.

Incidentally, the boolSimps.DNF_ss simpset fragment includes these
quantifier movements as well as the propositional rewrites that
convert to DNF.

Added to boolTheory: PULL_FORALL and PULL_EXISTS

manually log proofs for some thms with point-free Unwanted.id

and bump lazy-list opentheory package version

Allow case expressions to parse with leading bars. Closes #25.

add various names to the OpenTheory map

This is in preparation for logging llistTheory.

Notes:
- Sent combin$C to Function.Combinator.c (same for combin$S).
Another name might be preferred on the OpenTheory side.
- Not sure what bool$BOUNDED is about; dumped it in the HOL4 namespace.
- Put lots of pred_set constants in the Set namespace, but in the
standard (OpenTheory) library it seems like Set is for constants
operating on an abstract type of sets (rather than predicates). I'm
not sure whether we should use a different namespace when working with
sets-as-predicates or just pretend predicates are the abstract type
and do a bit of magic on article reading/writing as necessary (don't
know what that would be exactly yet).
- Similar for constants in set_relation, which I'm currently putting in
the Relation namespace. Although it looks like currently OpenTheory
doesn't use an abstract type of relations (but probably it will
later).
- Sent marker$Cong and marker$Abbrev to Unwanted.id, but not sure if
Unwanted.id is supposed to be polymorphic (whereas those are identity
functions restricted to bool). Similar for numeral$iZ
- sent GSPEC to Set.specification; maybe not an obvious name...
- Using top-level "While" namespace for whileTheory
- dumped numeral$iiSUC in HOL4 namespace; not sure what to do with it
- BIT2 is going to Number.Numeral.bit2; this is in line with wanting the
base library to be liberal, i.e. a union of all useful basic constants
and theorems (so has bit0, bit1 and bit2)... but I think there may be
competing goals for base

opentheory name for bool$DATATYPE

might want to think about stripping tags like this later, though

Successfully parse case expressions of 0, 1 or 2 alternatives.

Parsing more alternatives: broken.
Pretty-printing: broken.

However, this approach has the advantage that it won't give us
ambiguity error messages at any point, and won't conflict with the
original "double-barred" gspec2 syntax.

Adopt ML-style syntax for case expressions and use freed up "||" for bitwise-or. See issue #24.

better match intended semantics of OpenTheory names

rather than using strings, now have a type abbreviation otname for
string list * string. it might be worth writing more operations on this
type (like for manipulating the namespace).

Move fixities around for let, case and || forms. Fixes #19.

typo in boolTheory - arb is meant to be uppercase

add a few more names to the OpenTheory map

specifically, bool$ARB, bool$TYPE_DEFINITION, and some stuff from
ind_type

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

Example theories GilithBool and GilithUnit

These theories export each export a single theorem that is a conjunction
of all the exports of the articles for bool-1.0 and unit-1.0 in the
gilith repository. They use HOL's already-defined constants. The
GilithUnit example shows one way to use the exports from another
opentheory theory to satisfy the requirements of the current one.

Move only primitive bool stuff into new src/bool.

Expectation is that *Map stuff will also leave this directory eventually.

Add an OpenTheoryMap analogous to TexTokenMap

Also, add names for various type operators and constants in boolTheory,
listTheory, and numTheory so that the Opentheory selftests now pass without
having to set up those name mappings themselves.

Move bool parse tricks into boolTheory so that they appear in bool_grammars.

Add TeX notations for some HOL keywords: if-then-else, case-of, let-and-in and
do-od.

Rework grammar infrastructure, losing 'preference' for concrete syntax.

Instead, the most recent rule is the one the pretty-printer will prefer.
The clear_prefs function disappears, but the prefer_form function stays
because it can just adjust the timestamp on the desired form to be most
recent.

TeX macros in TeX_notation calls need to be terminated with {}.

Move more TeX notations into appropriate theory files.

Word-related notation still to do.

Move all of boolTheory's tokens into TexTokenMap, and use this in EmitTeX.

Still need to capture other theories' tokens similarly.

Start on new facility to define TeX information for HOL tokens in theory files.

Ultimately, this will replace the big function (called "string_map")
in TeX/EmitTeX.sml. I have started to annotate boolScript but the
information stored there is not yet used.

Reworked implementation of Unicode structure.

Unicode is now a sub-structure of Parse, with functionality provided
by a separate ProvideUnicode module. This organisation makes Parse
the primary module once again (previously Unicode built on top of
Parse).

Changes in src/bool result from

open Parse Unicode

not working. Instead the two opens must be in separate lines:

open Parse
open Unicode

Thm.ETA_CONV -> Drule.ETA_CONV, Thm.Eta -> Drule.RIGHT_ETA

Cursory profiling indicates that an implementation of ETA_CONV as a primitive
inference rule in Thm is about 20 times faster than an implementation as a
derived rule that instantiates ETA_AX, but that the difference in overall HOL
build time is negligible.

Please do let me know if you encounter (performance) problems due to this
change.

Added a very brief comment explaining ETA_AX vs. Thm.ETA_CONV, summarizing the recent discussion on the developers mailing list (in the hope that it wasn't completely in vain).

A proper fix for what r6851 attempted to fix. The problem was
demonstrated by ideaMultScript in examples/Crypto/IDEA. This loaded
its ancestor theory ExtendedEuclid before it loaded the ind_types
module. The problem is that ExtendedEuclid makes "P" a constant, and
ind_types attempts to prove a lemma internally where P has to be a
variable. Now, it also sets up its parser to be with respect to a
grammar not contaminated by ExtendedEuclid, so its statement of the
goal is fine.

The goal is

!P t. (!x. (x = t) ==> P x) ==> $? P

Unfortunately, when the tactic that comes to solve this goal calls

REPEAT GEN_TAC

the code in GEN_TAC spots the "P" and checks the *global* grammar for
clashes with known constants. P is such a beast, and so the goal
after the GEN_TAC is

(!x. (x = t) ==> P' x) ==> $? P'

A later tactic that mentions P (which is still parsed correctly as a
variable called "P") then causes the tactic to derail and the proof to
fail.

It's possible to make the tactic work by using X_GEN_TAC (but not
Q.X_GEN_TAC), but it's all terribly ugly, and so I decided to prove
the theorem in boolTheory, so that the *three* places where the same
code was being duplicated could pick up the theorem without reproving
it. I also removed the code duplication by making the one version in
Prim_rec the source for the two other users.

Now examples/Crypto/IDEA builds properly.

This fix will have to be merged into

branches/release-development/kananaskis-5

This does suggest, incidentally, that Konrad's solution to parsing
protection, involving setting the global grammar reference at the head
of library files, is pragmatically better, for all that futzing around
with references is ugly, and requires the end of the file to set the
global reference back to what it was (yergh). I will have to give up
on my "clean" solution, which rebinds/redefines the Parse structure at
the head of library files.

theorems COND_EXPAND_OR, COND_EXPAND_IMP and MONO_NOT_EQ added

Minor changes ... addition of a rewrite rule
about literal_case (which turns out not to
be needed).

Added Peirce's law, possibly useful for teaching.

Implement ML code generation for large records.

Make the pretty-printing of prefix forms nicer. Basically, when a
prefix form appears as the rand of a function application, it will
pick up parentheses. This means
f (if P then x else y)
will print with the parentheses (though they are redundant).
Similarly, for
f (!x. P)
The latter happened rarely enough that I previously bodged it by
having if-then-else always print with parentheses. The only other
prefix in the base system was ~, and here
f ~p
looks OKish. Now, we get
f (~p)
which I think is an improvement.

Fairly dramatic change, supporting the use of "syntactic patterns".
It is now possible to overload a name to term (typically a
lambda-abstraction) in order to create syntax-only definitions. For
example, there is a definition of not-equals now in the system:
val _ = overload_on ("<>", ``\x y. ~(x = y)``)
val _ = set_fixity "<>" (Infix(NONASSOC, 450))
This definition is parsed and pretty-printed.

Two other annoying changes. The interface for adding unicode variants
has changed, and I have made precedence level 450 of the parser
non-associative. This latter change has caused most of the (minor)
adjustments to the files below. The regression test doesn't go
through yet. (Currently there is a failure in
quotient/examples/sigma that I don't understand.)

Another fix to the way Unicode-overloading works. It now checks to
see if the term you are overloading to has an ASCII concrete syntax.
(For example, integer$int_le has an ASCII concrete syntax of <= as an
infix.) If so, it will set up the Unicode symbol as an alias for that
concrete syntax. This means that subsequent overloads on the same
ASCII symbol will also pick up the Unicode symbol.

Graphically, we have something like



x <= y +----- arithmetic$<=
\ |
>---> COMB(COMB(<=,x),y) >---+----- integer$int_le
/ |
x ≤ y +----- words$word_le
|
... etc

where the middle column is the result of Absyn applied to the given
quotation.

Modify Unicode to use an interface whereby theories can specify
Unicode alternatives for their constants. These can be turned on and
off by fiddling with the trace variable "Unicode". I.e., to see
pretty stuff, run hol and then
- set_trace "Unicode" 1;
> val it = () : unit

- FORALL_SIMP;
> val it = <...pretty stuff...>
I haven't gone through and done the words because it's time for me to
go home.

Remaining issues:
* type abbreviations
* the lambda binder (this is not a constant, so we can't use
overloading)
* restricted quantifiers
* whether automatically having Unicode stuff in the grammar (even if
disabled) might cause non-Unicode users pain

Deleted use of AND_CONG and OR_CONG from the
standard set of congruence rules. They had
the tendency to make ordinary recursions look
like very strange nested recursions. If congruence
rules are needed for recursing under /\
or \/, then probably LEFT_AND_CONG and LEFT_OR_CONG
will suffice (they loosely capture left-to-right
evaluation).

Did some community service expunging all occurrences of the old syntax for
if-then-else from the HOL distribution.

Apologies if I've broken your example or development: you can either upgrade
it to use the new syntax or else issue the magic parser incantation that
I chopped out of boolScript.sml on this check in.

Random other bits deemed useful.

Fix bugs:
* a call to overload_on was being made in boolSyntax.sml, which prompted
the code in Parse.sml to complain about updates being thrown away. The
call in boolSyntax.sml should have been to temp_overload_on if anything.
But better still to put the call to overload_on in a theory file...
* Modified Parse.sml to report the throwing away updates error more verbosely.
* Putting the call to overload_on in boolScript caused an exception. This
happened because the pretty-printer was raising an exception when trying
to print literal_case_THM, featuring the term ``literal_case f x``.
(This was happening because the call to overload_on was making the
pretty-printer think that it should be treating such terms as case
expressions.) Fix this by removing the redundant code in term_pp.sml that
was attempting to do the printing and raising the wrong sort of exception
in the process. (Also add an exception handler to the call-out to the
provided case-expression destructor in the other branch, just to be
paranoid.)

----------------------------------------------------------------------
Enter Log. Lines beginning with `CVS:' are removed automatically

Committing in a new version of literal patterns and case expressions.
This includes a new constant, literal_case : ('a -> 'b) -> ('a -> 'b)
which wraps the previously constructed chains of bool_case expressions
that represent cases branching on literal patterns.

Modified Files:
hol98/src/bool/DefnBase.sml hol98/src/bool/Pmatch.sml
hol98/src/bool/TypeBasePure.sml hol98/src/bool/boolScript.sml
hol98/src/bool/boolSyntax.sig hol98/src/bool/boolSyntax.sml
hol98/src/parse/Preterm.sml hol98/src/tfl/src/Functional.sml
----------------------------------------------------------------------

Keeping \^ to mean an escaped form of ^ means that \^x. foo needs to be
rewritten to \ ^x. foo... This change can stand even if we back out this
change to the filter.

Prove theorems sufficient to make :'a itself a fully-fledged member of the
TypeBase community. This allows people to use Define to write
Define`myfn (:'a) = ...`
which is not as trivial as it looks because (:'a) is a constant, not a
variable.

Implement new "itself" type constructor and special syntax to represent
its one value. The syntax is ``(:'a)`` for the value belonging to type
'a itself. (Or ``(:bool)`` etc.)

Changes to make it easier to dispense with the let-and concrete syntax
and put something else there instead. Even without throwing them away
it is now possible to write ``$let`` and have this just be a variable of
type alpha, rather than a parse error. So that's an improvement.
If you wanted to define a constant "and", allowing this would be as
simple as chucking the rule for "and", by using
remove_termtok {term = GrammarSpecials.and_special, tok = "and"}
and then defining the new constant "and" with Define, and possibly
giving it fixities etc, as you might with any other constant. Similarly
for let.

Deleting funky HTML output from xTheory.sig files. I thought I had
removed all of this ...

Added equality versions of induction theorems. Sometimes this can
let you do induction proofs by rewriting. For example,

!L1 L2. LENGTH (L1 ++ L2) = LENGTH L1 + LENGTH L2

can be proved by RW_TAC list_ss [FORALL_LIST]. But just as
often it doesn't do the right thing ...

Hacking around to get HTML symbols put in generated `Theory.sig'
files. Allows usual logic symbols (and some set theory symbols)
in the generated html files, see help/HOLindex.html after a
complete build of the system (examine a theory file).

Only symbol not currently dealt with properly is lambda. Also,
I thought I had emptyset sussed, but it stopped working for
some reason ... not a problem since "{}" works just as well,
and may be nicer.

Alter the way BOUNDED/UNBOUNDED rewriting works, so that the BOUNDED
tag is now a theorem hypothesis of a special form, and so there is no
UNBOUNDED tag at all (i.e., the default is to be unbounded). This is
simpler, and means that if you come to write a simplifier filter (as
in the case of SUC_FILTER_ss) you don't need to worry about whether
or not the rewrite is bounded. (Will add this check-in message to
changed files in src/simp/src that got mistakenly tagged with my change
to selftest there.)

Added tag for generating theorems describing datatypes. Used for
interfacing to reFLect.

Two new theorems about RES_FORALL and RES_EXISTS. Put them into
BOOL_ss, and thus bool_ss, and anything else built on that foundation.

A fix for a bug in the simplifier's treatment of congruence rules that
prevented it from handling "higher order" rules, like this one for
RES_FORALL:

|- (P = Q) ==> (!x. x IN P ==> (f x = g x)) ==>
(RES_FORALL P f = RES_FORALL Q g)

Feeling brave, I then put this, and the accompanying rule for RES_EXISTS
into bool_ss. Congruence rules take precedence over normal term traversal
in the simplifier, so with a rule like the above installed, the constant
RES_FORALL is never "seen" on its own. In particular, this means that
you can't rewrite with RES_FORALL_DEF, which looks like

|- RES_FORALL = (\p m. !x. x IN p ==> m x)

Instead, you need to rewrite with something that matches at the same level
(or higher) as the congruence rule. Thus, RES_{FORALL,EXISTS,SELECT}_THM
in boolTheory. These can then be the basis for the theorems in
res_quanScript, and look like

|- RES_FORALL P f = !x. x IN P ==> f x

Support for rewriting annotations.

A bunch of long-deferred changes, of various impact. Main ones that
I can recall right now:

* fix to CONV_TAC for new fully-Boultonized conversions
* Adding encoders into TypeBase.

A new theorem; useful for doing DNF-like normalisations.

Added a very useful tactic for dealing with Hilbert-choice ($@) terms.

(With sadness :) removed the EXT_POINT constant: although rather cute,
it's a bit too specific for boolTheory.

If anyone's interested, it's being rehomed into normalFormsTheory, which
will someday find its way into the HOL distribution.

Added the EXT_POINT constant (see explanatory mail message to hol-developers).

Experimental addition of rewriting directives. Currently, only "Once"
or "Atmost" are allowed.

Overlay.sml now exports infix declarations for the "standard" infixes,
taken from std.prelude. This means that the infix component of the
standard Script boilerplate is unnecessary. Updated Manual documentation
to reflect this. Changed combinScript and examples/ind_def/clScript.sml
just to show that it worked.

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.

Reverted to the more natural definition of RES_EXISTS_UNIQUE:

(?!x :: p. m x) = (?x :: p. m x) /\ (!x y :: p. m x /\ m y ==> (x = y))

and derived the shorter definition in RES_EXISTS_UNIQUE_ALT:

(?!x :: p. m x) = ?x :: p. m x /\ !y :: p. m y ==> (y = x)

Restricted quantifier definitions are now in boolTheory.

Added FORALL_THM and EXISTS_THM.

Minor modifications, prompted by Joe

Removed the dependency of proof of MONO_AND on order of hypotheses.

Minor changes to accomodate new tweaks to representation of nested
recursions. It was wrong before, and horribly clumsy.

Modifications to implement parsing and printing of case expressions.

Better installation of case concrete syntax.

Added pattern-matching code from tfl, and "magic" case constants to
boolScript. TypeBase also initialises case information function with
Preterm module.

Added a theorem about bool_case to boolTheory, and added API
support for bool_case terms.

Minor alterations.

Thanks to Joe Hurd, have moved his theorems for case analysis on all
(4) functions of type bool -> bool into boolScript.

Minor changes. Hol88Subst has been incorporated into hol88Lib.

Paired syntax.

Latest updates. Almost everything is in paired syntax now, except for
substitutions.

* fixed bug in strip_{conj,disj} (neither broke apart
left-associated bits).
* added ONTO_THM and ONE_ONE_THM to boolScript to provide theorems
analogous to old forms of ONTO_DEF and ONE_ONE_DEF (by analogy
with what was done with TYPE_DEFINITION/TYPE_DEFNIITION_THM).

New stuff in bool. Theory script has changed a little; big change is
addition of stuff that all used to be part of basicHol90Lib. Now that
is all done here. The theory "min" is now also strictly virtual, having
its grammar defined in parse, and its constants assumed.

Altered the precedence of let to be less than that of the old style
conditional expression. Now let has broadest possible scope.

A couple of miserable new theorems about ?!.

Changes due to move of hide/show information from Parse_support list
into grammars.

Added some congruence theorems for implication, conjunction,
disjunction, if-then-else, and let expressions.

Many additions, from Ho_boolScript. I intend to keep beavering away at it
until everything there has been moved into boolScript.sml, but that
requires forward proofs, which take time.

proof of IMP_ANTISYM_AX using BOOL_CASES_AX.
explicited actual dependencies of some derived rules of Thm

Minor changes.

Added distribution laws for LET. And LET_THM.

Revised pretty-printing for if-then-else form of conditional expression.
Lost ability to have
if P then Q
else R
If a break is necessary it will print as
if P then
Q
else
R
or at worst, as
if
P
then
Q
else
R
This fix is good though because it prevents
if P then
Q else R
Also made it always parenthesise these terms. Without parentheses multiply
nested if-then-elses become near impossible to read.

Minor change caused by shift of all the _special variables to the separate
GrammarSpecials structure.

Fixed up pretty-printing of if-then-else. It now looks pretty good.

Updates for new pretty-printing support. In boolTheory this has impacted
the treatment of if-then-else.

Changes necessary to make :: an infix operator representing CONS as well
as the restricted quantification operator. This change has required some
changes to the basic design of the parser; it's now not possible to have
more than one res. quan. operator.

Made the old style conditional operator low enough precedence so that it
can co-exist when set comprehension is introduced.

Added _COMM names for theorems hitherto called _SYM, i.e., there are now
available CONJ_COMM and DISJ_COMM.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)

Added new DISJ_IMP_THM |- !P Q R. P \/ Q ==> R = (P ==> R) /\ (Q ==> R)

Introduced a comment suggesting that I will add a proof of DISJ_IMP_THM
in here. Haven't done it yet.

Initial revision