special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;

more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;

suppress short abbreviations more uniformly, for outer and quasi-outer syntax; tuned signature;

clarified init_assignable: make double-sure that initial values are reset; more systematic reports for Args.syntax: indicate Args.$$$ quasi-keywords and suppress confusing completion of single symbols like ":", "|", "?";

proper UTF-8;

fix typo

remove simp rules made redundant by the replacement of neg_numeral with negated numerals

tuned proof

tuned proof script

no 'sorry' so that the schematic variable gets instantiated

removed junk

simplify sets in BNF composition

tuning

more caching in composition pipeline

register relator equations as spec rules only for datatypes -- for codatatypes they underspecify the function and are therefore dangerous (e.g. to Nitpick)

updated docs

renamed a pair of low-level theorems to have c/dtor in their names (like the others)

propagate the exception that is expected later on

N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;

merge

removed debugging leftover

minor doc fix

added contributor

simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls

fixed handling of 'case_prod' and other 'case' functions for interpreted types

updated docs

support 'datatype_new'-defined datatypes in Nitpick + better support for 'codatatype's

tuned ML names

tuned code

removed nonstandard models from Nitpick

more code lemmas by Rene Thiemann

merged;

tuned proofs;

tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);

recovered position hyperlinks from 65c9968286d5 (NB: "def" position vs. regular one);

tuned messages and markup;

test polyml-svn;

README is optional in test compilations;

clarified path checks: avoid crash of rendering due to spurious errors;

more precise navigation within open files;

tuned signature;

tuned signature;

updated NEWS

guard against unsound cases that arise when people peek into 'int' and similar types that are handled specially by Nitpick

adapted example

removed obsolete, harmful step in tactic

removed (co)iterators from documentation

avoid duplicate 'disc_iff' theorems

rationalized internals

rationalized internals

rationalized internals

life without 'metis'

rationalized internals

rationalized internals

rationalize internals

optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant

compile

make 'diff_iff' a simp rule if available

less aggressive resolving

repaired argument list to corecursor

adapted to absence of 'unfold'

got rid of automatically generated fold constant and theorems (to reduce overhead)

use same identity function for abs and rep (doesn't seem to confuse any proofs)

make 'typedef' optional, depending on size of original type

use aconv to compare terms (for cleanliness)

tuning

optimize cardinal bounds involving natLeq (omega)

no extend_word for now, it is in conflict with manual reformatting of sources via TAB (e.g. accidental replacement of 'assume' by 'assumes');

merged

more standard module name;

silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;

tuned whitespace;

allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;

tuned proofs;

prefer Name_Space.check with its builtin reports (including completion);

tuned source structure;

prefer Name_Space.check with its builtin reports (including completion);

consider completion report as part of error message -- less stateful, may get handled;

more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;

more antiquotations;

clarified names of antiquotations and markup; more documentation;

tuned proof

merged

tuned proofs

repaired document;

repaired document;

more markup for ML source;

merged

tuned signature;

clarified language markup: added "delimited" property; type Symbol_Pos.source preserves information about delimited outer tokens (e.g string, cartouche); observe Completion.Language_Context only for delimited languages, which is important to complete keywords after undelimited inner tokens, e.g. "lemma A pro";

clarified module structure;

tuned;

tuned signature -- separate module Font_Info;

tuned;

font size change with delay, to avoid GUI lagging behind user input;

incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace); tuned signature;

more symbols, less parentheses;

tuned signature -- more explicit Document.Elements;

made SML/NJ happier

more precise imports; avoid duplicated simp rules in fact collections; dropped redundancy

earlier setup of transfer, without dependency on psychodelic interpretations

cursory polishing: tuned proofs, tuned symbols, tuned headings

merged

tuned whitespace; more symbols;

allow completion within a word (or symbol), like semantic completion; no special treatment for History_Text_Field, due to lack of active range rendering;

more regular buffer_range, despite 47e8c8daccae; more robust invalidate_range, which is relevant when editing at the end of the buffer (NB: last line offset by be outside actual buffer length);

load Metis a little later

made SML/NJ happier

merged

added Rene Thiemann's patch for the nonterminating equality/subset test code for multisets

added function "List.extract"

explicit link to Z3 license;

recovered minimal README from 30de372ca56f;

adapt examples to new intermediate typedef

joint work with blanchet: intermediate typedef for the input to fp-operations

prefer abstract datatype -- in accordance to ML version;

tuned data structure;

tuned;

tuned comment;

tuned signature;