Renamed `rich_topologyTheory` to `real_topologyTheory`

Merged hol-light's cardTheory (rich_cardinalTheory) with HOL4's cardinalTheory

Revised next release notes according to PR comments

Mention the new `topologyTheory`, `metricTheory` and `rich_topologyTheory` in next release notes

Document ee54b084d's change in release notes

Change Holmake to use "quit-on-failure" by default

Document this and the new --noqof option that allows the old behaviour
to be restored.

Closes #576

Create new blank next-release.md for filling in before next release

Label release notes with Kananaskis-12 name

Fix up move of hol_sets into src: de-Unicodification; fix one ref

Mention this in release notes.

added release note for regexpLib

Implement easier API entrypoints to get at case_eq theorems

Closes #345

Implement Haskell-style $ as infix function application operator

With documentation and some simple test cases.

release notes: finish a sentence with a full-stop

Fixed wrong links in TOC of next-release.md

Added Lambek Calculus formalization into HOL example, under `formal-languages`.

Change irule to not include a rpt conj_tac effect

Closes #465

Mention ANSI colour configuration in release notes

Add more to release notes

Text on new examples:
- Chun Tian's CCS work
- The Tamarack port from HOL88

Other minor things also.

Mention Simon Jantsch's LTL example in release notes

Updated release notes with monad-syntax, mention of CCS example

Mention new xTheory.dat files in release notes

Fix TeX p/printing bug caused by having multiple types of same name

If the types had different arities, mungers would produce strange
mk_type exceptions.

Remove -- as an alias for Term parser.

As per comment in release notes this has long been replaced as
appropriate style.

Improving naming of bit-vector signed division constants.

This renaming introduces incompatibilities:

• words$word_sdiv -> words$word_quot (this is proved to be related to int_quot for a non-zero divisor).
• words$word_srem -> words$word_rem (this is proved to be related to int_rem for a non-zero divisor).
• integer_word$word_sdiv (this is a new constant defined directly in terms of int_div).
• words$word_smod -> integer_word$word_smod (this is now defined directly in terms of int_mod).

Fix Q.GENL to handle variables in same order as GENL.

Closes #428

Move Q.ID_EX_TAC to Tactic.

ID_EX_TAC doesn't take any arguments, let alone a quotation, so
doesn't belong in Q.

Closes #359

Mention length-nil change in release notes

Provide more advice on dealing with the new by in release notes

Put my byfix.pl script into the release notes

Document availability of byA in release notes

Document changes to by and new subgoal tactic

Also make sure that the latter (and its alias, sg) are available
through the bossLib signature.

Adjust fixities of finite map composition operators

Incorporate new c/line option-handling into build

The build in relocation option doesn't do anything at the moment.

Document TAKE/DROP change in release notes

Mention the one-line method for restoring old behaviour

Add MOD_ss to srw_ss()

If it breaks proofs, this is easy to reverse in a script by doing

val _ = diminish_srw_ss ["MOD_ss"]

before the old behaviour is being relied upon

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.

Document Holmake's concurrency in release notes

Document change to qpat_assum and friends

Document the incompatibility introduced by 30f78bd

Fix another record pretty-printing problem

Fix thm_to_string to use raw backend properly.

The term_to_string and type_to_string functions do this already.

Remove state_option theory.

Documented in release notes, including pointer to errorStateMonad
theory.

Release notes (Holyhammer)

add some release notes for gen_new_specification

Correct URL in release notes

Grammar correction in release notes

Let load work if current directory is unwritable

Prevent bad constant names at Definition level

Enforces a constraint I'd long assumed to be true.

Closes #268

rename example "deep_matches" to "pattern_matches"

The name is confusing. The pattern compilation is in some
rather vague sense deep, not the case-expressions. Moreoever,
the lib grew since it was named such that the deep pattern
compilation is not its most prominent feature any more.

Mention github issue #260 in release notes

Let PAT_ABBREV_TAC use patterns that are more polymorphic than the goal

Closes #252

Datatype now handles antiquotations.

Closes #258

Datatype: qual-ids stop creation of recursive type

Closes #257

Implement HOL Light's {PAT,PATH}_CONV.

Closes #255

Tweaks to pattern-match example release notes

Including
- use Unicode apostrophe
- put one sentence per line
- indent so as to make pandoc happy
- some grammar

document deep_matches example in release notes

Make Holmake follow INCLUDES recursively, even when given PHONY target

Closes #145

Fix a Markdown error in release notes.

Document fix to issue #225 (constructor names for theorems)

Change API of Q's MATCH...RENAME_TACs.

Now rather than a string list hanging off the end specifying which
variable bindings aren't supposed to induce a renaming, just put
underscores into the pattern in those positions.

Documentation and release notes updated.

Modify optionSyntax.dest_none to unwrap the type returned.

Closes #215.

Fix & document an infinite loop bug in intSimps.{OMEGA,COOPER}_ss

Problem was that the term F was viewed as suitable context for the
simplifier's decision procedure. Though superficially reasonable, this
leads to problems because the simplifier will rewrite everything it
can inside this context to F, using the rewrite

[F] |- somegenvar = F (1)

but the integer decision procedures will correctly rewrite occurrences
of F to T, because the underlying conversion is happy to prove

|- (F ==> F) <=> T

The natural number procedure in ARITH_ss doesn't suffer from this
problem because it doesn't add F as context to the decision
procedure's context, and that's the fix taken here.

The decision to use (1) above rather than rewrite to true, say, was
taken in 9bc4bdaa.

Mention balanced_bst example in release notes.

Empty command-line Holmake only builds first target in Holmakefile.

If there is no Holmakefile, or if there is a Holmakefile with no
targets, then the old behaviour of attempting to build everything
possible happens.

Documented in release notes and DESCRIPTION.

Many of the distribution's Holmakefiles were harmed in the creation of
this commit, but, for the reasons given in the release notes, I don't
think this should happen that often for typical user developments.

Closes #175

Minor formatting tweak in release notes.

Pretty-printer now annotates consts with their real names and types.

In "complicated" overload situations, such as the overloads for NOTIN
and <>, the annotation can't point to a "real" underlying constant,
but does still provide the type for the emacs tool-tips.

In passing, also create a new annotation form, the SymConst as well as
the Const. This is done for the TeX backend's benefit, so that it can
avoid treating things like + the same as normal identifiers. This
works well for math-mode munging where you want "+" to map to $+$, but
want "INSERT" to map to \textsf{INSERT}.

Closes #39

Document wildcard function in DESCRIPTION and release notes

add release note about custom compsets

Mention the sptree theory in the release notes.

mention update to vim mode in release notes

(not sure if that's the right section)

Mention new automatic rewrite, |- !v:one. v = () in release notes

Mention that the DESCRIPTION is also available in Italian.

Credit Piotr Trojanek for all of his documentation fixes.

Handle character literals when printing to LaTeX

Closes #190.

See also 89b5d3224403 for first piece of work in this vein.

Remove broken and unnecessary {temp_,}add_binder entry-points in Parse

Fix bug in pattern-matching within user-pretty-printers.

Closes #172.

Fix another examples/ proof broken by 875ba111.

Mention these automatic rewrites in release notes.

Minor polishing in release notes.

Add description of floating-point theories to release notes.

Thanks to Anthony for the raw material.

Tweaks to markdown in release notes so that pandoc copes with it.

Fix proof broken by new auto rewrite in 9ff04c4dc9.

This is evidence of a backwards incompatibility, so mention the change
in release notes.

Fix arithmetic d.p. mis-feature identified in c59783a4d0e3d

Issue was that conditional expressions with non-presburger guards
resulted in goals that weren't provable because ARITH couldn't handle
boolean sub-terms that weren't presburger. This prevented its
instance-generalisation mechanism from solving obvious goals like that
in the test-case.

Now the instance-generalisation mechanism will perform up to four
case-splits on boolean sub-terms. Of course, the choice of four is
completely arbitrary, but a possible 32-fold expansion in goal-size
seems unreasonable.

Document the change in the release notes.

Minor reformatting in release notes

Slight clarification of language about Datatype in release notes.

Rename implicational theorems in relation to make room for equivalences

This affects TC_CASES1 and TC_CASES2 that were hardly ever being used.
See the release notes change for more discussion.

Fix some examples broken by change to EmitML's handling of datatype decls.

Implement most of a new Datatype function with nicer syntax.

(Pair-programming with Magnus who wanted it.) Still need to
implement change to EmitTeX.

Put release date template/reminder into release notes

Define MAX_SET on the empty set to equal 0.

This make the relevant equation

FINITE s ==> (MAX_SET (e INSERT s) = MAX e (MAX_SET s))

Mention list range theory in release notes.

Extend simplifier's treatment of abbrevs to handle abstractions better

Minor updates to next release notes.

Notes for Lockwood Morris's enumerated finite sets/maps library.