subsumed by NEWS -- for older history, see previous versions of Nitpick

don't show spurious "..." in Nitpick's output for free variables of set type (e.g., P (op +) example from Manual_Nits.thy); undoes parts of 38ba15040455, which was too aggressive

honor xsymbols in Nitpick

added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"

document new option

make Nitpick handle multiple typedef entries for same typedef

remove comment

thread along context instead of theory for typedef lookup

obsolete FIXME

move SAT solver warning from every invocation of SAT solver to the tool, Refute, that uses it; "size_change" rarely needs anything beyond "dpll", so this warning is annoying at best, and when "size_change" is called from Nitpick the warning confuses users, who then think that Nitpick is using "dpll" when it's really using MiniSat or some other fast solver

don't include any axioms for "TYPE" in Nitpick

dropped obsolete script

normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);

merged

avoid store flag in add_* operations

arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML; misc tuning;

merged

do not expose store flag of AxClass.add_*

merged

adapted to changes

capitalized type variables; added yield as keyword

brackify_infix etc.: no break before infix operator -- eases survival in Scala

basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short;

use local /home/isatest/polyml-5.3.0 on atbroy102 to avoid problems with the SMB filesystem via homebroy;

uniform ML environment setup for Isar and PG;

merged

Renamed TypeInfer to Type_Infer.

merged

assign now applies meet before update_new to avoid misleading error message.

Tuned.

Adapted to new format of proof terms containing explicit proofs of class membership.

classrel and arity theorems are now stored under proper name in theory. add_arity and add_classrel take extra boolean argument indicating whether theorems should be stored.

- outer_constraints with original variable names, to ensure that argsP is consistent with args - Exported map_proof_same, added implies_intr_proof' and forall_intr_proof' - Rewriting procedures used by rewrite_proof can now access hypotheses - Finally enabled unconstrain

outer_constraints with original variable names, to ensure that argsP is consistent with args

- Equality check on propositions after lookup of theorem now takes type variable renamings into account - Unconstrain theorem after lookup - Improved error messages for application cases

Use Proofterm.forall_intr_proof' instead of locally defined forall_intr_prf.

- Added extra flag to read_term and read_proof functions that allows to parse (proof)terms in which all type variables have the top sort - Adapted proof_of_term to handle proofs with explicit class membership proofs

merged

merged

corrected printing of characters

corrected implementation

added Scala code setup

tuned code setup

keep structure ThyLoad for the sake of Proof General;

added random instance for word

notes on Isabelle/jEdit;

remove presently unused Isabelle application;

modernized some structure names, keeping a few legacy aliases;

merged

merge

fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option

updated generated files

clarified

adjusted

terminate ML compiler input produced by ML_Lex.read (cf. 85e864045497);

Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;

merged

Typo in locales tutorial.

Theory_Target.pretty: more markup;

tuned abbrevs for long arrows, according to usual ASCII syntax;