Fix printing of boolean negation after numeric types are loaded

If you have a term ~p /\ q, it should print as ¬p ∧ q (assuming
Unicode is enabled).

This wasn't true previously because of the dance around use of ~ as
numeric negation. The desired behaviour:

Parsing:

~ is preferentially parsed as boolean negation
¬ is only parsed as boolean/word negation
- (unary) is only parsed as numeric negation

Printing (with Unicode):
~ is never printed
¬ is printed for boolean/word negation
- (unary) is printed for numeric negation

Printing (without Unicode)
~ is printed for boolean/word negation
- (unary) is printed for numeric negation

Inspired to fix by reporting of issue #871

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.

removing tactictoe mini replacing by a tactic prioritization

Mention two new examples in release notes

Correct typos/reformat in release notes and math.stex

Documentation for product measure and Fubini's theorem

Update documentation of Holmake's recursive behaviours

Related to github issue #382

update next-release.md

Document nub simp changes from e85907d844; fix script broken by it

Document change to abbreviation behaviour in release notes

align numeric syntax: 'great' becomes 'greater' The earlier names are inconsistent with numSyntax and less descriptive.

The changes are:
intSyntax.great_tm -> intSyntax.greater_tm
intSyntax.dest_great -> intSyntax.dest_greater
intSyntax.mk_great -> intSyntax.mk_greater

int_arithTheory.add_to_great -> int_arithTheory.add_to_greater

realSyntax.great_tm -> realSyntax.greater_tm
realSyntax.dest_great -> realSyntax.dest_greater
realSyntax.mk_great -> realSyntax.mk_greater

github issue #629

Fix another proof (last at -t2) broken by a9a7e76c1

Also document backwards incompatibility in release notes.

Document new <<- (mlet) syntax in DESCRIPTION and release notes

Cleanup of append thms for SORTED

Product measure and Tonelli's theorem

Note the removal of rich_listTheory.REVERSE in release notes (Incompatibilities); all -t2 tests passed.

Updated HOL Description for mathematical theories (with other cumulative fixes)

Release notes for list+rich_list theory changes

Holwrap (#758)

* add holwrap tool

* Add holwrap to release notes

* added comment about multiline input

Minor typo/grammar corrections in release notes

AKS mechanisation (#750)

* Add to examples: AKS, with algebra and simple_complexity.

Added `derivativeTheory` and `integrationTheory` into release notes

Correct typo in release notes

The new HOL-Probability based on [0,+Inf]-measure theory (#735)

* The new HOL-Probability based on [0,+Inf]-measure theory

* Noted the new HOL-Probability in next-release notes;
Added a dedicated README.md in `src/probability`.

Add special Overload syntax to map to overload_on

Use in a few random places in src and examples, and document in
release notes and DESCRIPTION.

Allow "local" attribute to be added to Type syntax

This generates a temp_type_abbrev/temp_type_abbrev_pp call underneath.
Document and use in a few src files.

Thanks to Magnus for the suggestion.

Further document drule breakage by linking to CakeML's old_drule

release notes: italicise REFERENCE and DESCRIPTION

This is better compatible with the ancient tradition for typesetting
these names.

release notes: describe drule incompatibility & fix more accurately

Document drule change from 812a08a5

Document new Datatype and Type syntaxes

Fixed wrong spelling of names, sorry.

Moved BISIM(_REL) theorems to bisimulationTheory with coinduction principles added

Mention compactness example in release notes

Also put it into build sequence and add a README file in the directory
itself.

Mention incompatibility of foo_def_compute turning into foo_compute

(Refers to change in f12ce51af.)

Extend and move theory of lists-of-nats encoded as nats

Previously, there was a rudimentary script in examples/computability's
prnlistTheory, which was used only in the computability tree. It's
useful to have all this stuff more widely available. (For example, in
showing Lowenheim-Skolem, setting up a bijection between the nats and
formulas is needed.)

New theory is now src/list/src/nlistTheory.

Thanks to Yiming Xu and Elliot Catt for help developing this theory.

Implement INST_TYPE facility within Q.SPEC_THEN

Closes #718

Add CoInductive syntax (mirroring Inductive syntax)

Progress with Github issue #711

Document new Inductive syntax in release notes

bug fixed + new tools

Announce add_strliteral_form in release notes

Clean up MEM_DROP situation

Problems:
- listTheory's MEM_DROP was horrible with a non-rewritable conclusion
- rich_listTheory had a MEM_DROP as well, which was weaker than the
same theory's MEM_DROP_IMP.

Fix:
- state a different MEM_DROP theorem in listTheory
- delete rich_listTheory's MEM_DROP

Move DEFAULT_TARGETS write-up to new features part of release notes

It had somehow ended up in the "New theories" section, perhaps as a
side effect of a merge.

Remove older of Theorem syntaxes (the one with the quotes)

It's confusing to allow two, and it seems pretty clear that the
Proof-QED proof is nicer.

Implement new Definition syntax; use it in src/sort and Tutorial

Move allow_schema_definition flag out of Globals into a feedback trace

This flag is used to allow schematic definitions, but in HOL is never
referred to outside of TotalDefn. People are using the
DefineSchema entrypoints instead.

Point out that setting loose equality affects descendent theories

This makes it easier to fix large theories given tight equality
because it means that one can dodge having to touch every script file.

Document some changes to emacs mode

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

Closes #680

Document removal of rewrites feature in release notes

Make Holmake c/line arg. "fooTheory" be treated as "fooTheory.dat"

This aims to make it easier for people to make specific theories
without needing to appreciate the fooTheory.{sig,sml,ui,uo,dat}
gawp. (Longer term, it would be great to hide/merge some of those
files entirely.)

Documented in the Holmake chapter of the DESCRIPTION manual, and
release notes. Tested in tools/Holmake/tests/theorytarget.

Document "thm-rebinding drop attributes" change in release notes

Document change to goal-printing defaults in release notes

Document tight equality change in release notes

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.

Document remove-term-eqtype change in release notes

Document theorem syntaxes in the release notes

Document DEFAULT_TARGETS variable in manual and release notes

Remove Globals.priming.

Also remove references to it in code that isn't being tested in the
regression checking build-sequence, and so is probably bit-rotted.

Provide numvariant version of variant, which behaves like

with_flag(Globals.priming,SOME "") (variant avoids)

Document change/incompatibility in release notes.

Change type_abbrev to not alter printing behaviour

If printing of abbreviations is desired, users must now use
type_abbrev_pp.

Closes #599

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.