Added documentation for the temporal_deep example

Document the new words theory, and the 'a itself type. (Also move all
</pre> tags to the beginning of the lines they occur on; this makes a visible
difference on the layout, at least within Firefox.)

HolBddLib makes a more sophisticated use of tags than I catered for with the
API change, so I've had to add a new function to Thm called add_tag (which
does the obvious). The implementation of PrimitiveBddRules changes slightly,
but its API remains the same.

Update the type of mk_oracle_thm so that it takes a string rather than a
tag as first argument. This is to prevent the following scenario:

- show_tags := true;
> val it = () : unit

- val ax = new_axiom ("foo", ``T``);
> val ax = [oracles: ] [axioms: foo] [] |- T : thm

- val th = mk_oracle_thm (Thm.tag ax) ([], ``F``);
> val th = [oracles: ] [axioms: foo] [] |- F : thm

Add notes for new type abbreviation printing feature. Slightly adjust
other entries (thanks for these, Peter and Mike) to make HTML validate.

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

Committing in release notes for XEmacs support and for literals in
case expressions.

Modified Files:
kananaskis-4.release.html
----------------------------------------------------------------------

Added acl2 example. Thought I'd checked this in a few days ago,
but checkin must have failed, so trying again.

Change to the inductive relations definition code to support a global, and
updated "monoset", which can be updated as theories load, thereby invisibly
increasing the capabilities of Hol_reln. Also simplify the implementation
of derive_strong_induction, and move the entrypoint to IndDefLib. New
test in src/IndDef/selftest.sml wouldn't have passed before (I believe).
It is more onerous than Peter's original monoset example, which didn't
feature recursion under the EVERY operator. Documented in Description and
release notes. Still to update theories with appropriate calls to
export_mono. (export_mono and export_rewrites are now part of bossLib's
interface.)

Update discussion of caret-escapes to reflect fact that ``s1 ^ s2`` is now
legitimate.

Fix and document bug found by Mike relating to string_EQ_CONV failing.
Fix is to use fromHOLstring rather than dest_string to check if terms
are string literals.

Minor clean-ups in release document, and addition of paragraphs on
new features in handling of quotations and string literals.
If you have a example that you want mentioned in the release notes, please
edit this file and put it in!

Fix a problem identified by Tom Ridge with the --rebuild_deps flag to
Holmake. Now the behaviour of this flag is to just call Holmake cleanDeps
before proceeding with the rest of its build.

Updates brought on by the change to the behaviour of ARITH_ss etc.

Update documentation to reflect Konrad's TypeBase changes.

Wide-ranging change to make the TypeBase export an interface forcing users
to be concerned about which theory their types are from. Interactive users
of the "induction_of", "axiom_of" and similar functions are thrown the only
bone: they can effectively omit the theory parameter by using "" instead
of a theory name.
Prompted by a bug found by Tom Ridge where it was impossible to define
a pattern matching function on a type with the same name as another type
because the pattern-matching code was using dest_type and TypeBase.read
on just the type-operator name.

Implement and document a new, unambiguous set comprehension syntax.
Only fixes required are to ieeeScript where old style =>-| if-then-else
syntax was nested to extraordinary degree without any parentheses.
Adding parentheses was the only thing required to fix the problem.

Document change to std_ss.

Document latest bug fixes.

Document EXISTS bug, and put a regression test into src/q to stop it
recurring.

Our first bug (and fix).