2014-03-03 blanchet 2014-03-03 removed nonstandard models from Nitpick
2014-03-03 nipkow 2014-03-03 more code lemmas by Rene Thiemann
2014-03-03 wenzelm 2014-03-03 merged;
2014-03-03 wenzelm 2014-03-03 tuned proofs;
2014-03-03 wenzelm 2014-03-03 tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
2014-03-03 wenzelm 2014-03-03 recovered position hyperlinks from 65c9968286d5 (NB: "def" position vs. regular one);
2014-03-03 wenzelm 2014-03-03 tuned messages and markup;
2014-03-03 wenzelm 2014-03-03 test polyml-svn;
2014-03-03 wenzelm 2014-03-03 README is optional in test compilations;
2014-03-03 wenzelm 2014-03-03 clarified path checks: avoid crash of rendering due to spurious errors;
2014-03-03 wenzelm 2014-03-03 more precise navigation within open files;
2014-03-03 wenzelm 2014-03-03 tuned signature;
2014-03-03 wenzelm 2014-03-03 tuned signature;
2014-03-03 blanchet 2014-03-03 updated NEWS
2014-03-03 blanchet 2014-03-03 guard against unsound cases that arise when people peek into 'int' and similar types that are handled specially by Nitpick
2014-03-03 blanchet 2014-03-03 adapted example
2014-03-03 blanchet 2014-03-03 removed obsolete, harmful step in tactic
2014-03-03 blanchet 2014-03-03 removed (co)iterators from documentation
2014-03-03 blanchet 2014-03-03 avoid duplicate 'disc_iff' theorems
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 life without 'metis'
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-03-03 blanchet 2014-03-03 rationalize internals
2014-03-03 blanchet 2014-03-03 optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant
2014-03-03 blanchet 2014-03-03 compile
2014-03-03 blanchet 2014-03-03 make 'diff_iff' a simp rule if available
2014-03-03 blanchet 2014-03-03 less aggressive resolving
2014-03-03 blanchet 2014-03-03 repaired argument list to corecursor
2014-03-03 blanchet 2014-03-03 adapted to absence of 'unfold'
2014-03-03 blanchet 2014-03-03 got rid of automatically generated fold constant and theorems (to reduce overhead)
2014-03-03 blanchet 2014-03-03 use same identity function for abs and rep (doesn't seem to confuse any proofs)
2014-03-03 blanchet 2014-03-03 make 'typedef' optional, depending on size of original type
2014-03-03 blanchet 2014-03-03 use aconv to compare terms (for cleanliness)
2014-03-03 blanchet 2014-03-03 tuning
2014-03-03 blanchet 2014-03-03 optimize cardinal bounds involving natLeq (omega)
2014-03-03 wenzelm 2014-03-03 no extend_word for now, it is in conflict with manual reformatting of sources via TAB (e.g. accidental replacement of 'assume' by 'assumes');
2014-03-02 wenzelm 2014-03-02 merged
2014-03-02 wenzelm 2014-03-02 more standard module name;
2014-03-02 wenzelm 2014-03-02 silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;
2014-03-02 wenzelm 2014-03-02 tuned whitespace;
2014-03-02 wenzelm 2014-03-02 allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;
2014-03-02 wenzelm 2014-03-02 tuned proofs;
2014-03-02 wenzelm 2014-03-02 prefer Name_Space.check with its builtin reports (including completion);
2014-03-02 wenzelm 2014-03-02 tuned source structure;
2014-03-02 wenzelm 2014-03-02 prefer Name_Space.check with its builtin reports (including completion);
2014-03-02 wenzelm 2014-03-02 consider completion report as part of error message -- less stateful, may get handled;
2014-03-02 wenzelm 2014-03-02 more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;
2014-03-02 wenzelm 2014-03-02 more antiquotations;
2014-03-02 wenzelm 2014-03-02 clarified names of antiquotations and markup; more documentation;
2014-03-02 nipkow 2014-03-02 tuned proof
2014-03-02 nipkow 2014-03-02 merged
2014-03-02 nipkow 2014-03-02 tuned proofs
2014-03-02 wenzelm 2014-03-02 repaired document;
2014-03-02 wenzelm 2014-03-02 repaired document;
2014-03-02 wenzelm 2014-03-02 more markup for ML source;
2014-03-01 wenzelm 2014-03-01 merged
2014-03-01 wenzelm 2014-03-01 tuned signature;