Tue, 04 Mar 2014 18:57:17 +0100 blanchet register relator equations as spec rules only for datatypes -- for codatatypes they underspecify the function and are therefore dangerous (e.g. to Nitpick)
Tue, 04 Mar 2014 18:57:17 +0100 blanchet updated docs
Tue, 04 Mar 2014 18:57:17 +0100 blanchet renamed a pair of low-level theorems to have c/dtor in their names (like the others)
Tue, 04 Mar 2014 13:38:02 +0100 traytel propagate the exception that is expected later on
Tue, 04 Mar 2014 12:32:33 +0100 traytel N2M does not use the low-level 'fold'; removed the latter from the fp_result interface;
Tue, 04 Mar 2014 10:35:37 +0100 blanchet merge
Tue, 04 Mar 2014 09:29:56 +0100 blanchet removed debugging leftover
Tue, 04 Mar 2014 09:07:49 +0100 blanchet minor doc fix
Tue, 04 Mar 2014 08:19:04 +0100 nipkow added contributor
Mon, 03 Mar 2014 23:05:49 +0100 blanchet simplified N2M code now that 'fold' is no longer used by the sugar layer + use right context in all 'force_typ' calls
Mon, 03 Mar 2014 23:05:30 +0100 blanchet fixed handling of 'case_prod' and other 'case' functions for interpreted types
Mon, 03 Mar 2014 22:33:22 +0100 blanchet updated docs
Mon, 03 Mar 2014 22:33:22 +0100 blanchet support 'datatype_new'-defined datatypes in Nitpick + better support for 'codatatype's
Mon, 03 Mar 2014 22:33:22 +0100 blanchet tuned ML names
Mon, 03 Mar 2014 22:33:22 +0100 blanchet tuned code
Mon, 03 Mar 2014 22:33:22 +0100 blanchet removed nonstandard models from Nitpick
Mon, 03 Mar 2014 16:44:46 +0100 nipkow more code lemmas by Rene Thiemann
Mon, 03 Mar 2014 15:14:00 +0100 wenzelm merged;
Mon, 03 Mar 2014 13:54:47 +0100 wenzelm tuned proofs;
Mon, 03 Mar 2014 12:54:12 +0100 wenzelm tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);
Mon, 03 Mar 2014 12:24:14 +0100 wenzelm recovered position hyperlinks from 65c9968286d5 (NB: "def" position vs. regular one);
Mon, 03 Mar 2014 12:18:59 +0100 wenzelm tuned messages and markup;
Mon, 03 Mar 2014 12:14:47 +0100 wenzelm test polyml-svn;
Mon, 03 Mar 2014 11:58:55 +0100 wenzelm README is optional in test compilations;
Mon, 03 Mar 2014 11:58:07 +0100 wenzelm clarified path checks: avoid crash of rendering due to spurious errors;
Mon, 03 Mar 2014 11:37:06 +0100 wenzelm more precise navigation within open files;
Mon, 03 Mar 2014 10:59:33 +0100 wenzelm tuned signature;
Mon, 03 Mar 2014 10:41:58 +0100 wenzelm tuned signature;
Mon, 03 Mar 2014 14:22:35 +0100 blanchet updated NEWS
Mon, 03 Mar 2014 12:58:17 +0100 blanchet guard against unsound cases that arise when people peek into 'int' and similar types that are handled specially by Nitpick
Mon, 03 Mar 2014 12:48:20 +0100 blanchet adapted example
Mon, 03 Mar 2014 12:48:20 +0100 blanchet removed obsolete, harmful step in tactic
Mon, 03 Mar 2014 12:48:20 +0100 blanchet removed (co)iterators from documentation
Mon, 03 Mar 2014 12:48:20 +0100 blanchet avoid duplicate 'disc_iff' theorems
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet life without 'metis'
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalize internals
Mon, 03 Mar 2014 12:48:20 +0100 blanchet optimized simple non-recursive datatypes by reusing 'case' for 'rec' constant
Mon, 03 Mar 2014 12:48:20 +0100 blanchet compile
Mon, 03 Mar 2014 12:48:20 +0100 blanchet make 'diff_iff' a simp rule if available
Mon, 03 Mar 2014 12:48:20 +0100 blanchet less aggressive resolving
Mon, 03 Mar 2014 12:48:20 +0100 blanchet repaired argument list to corecursor
Mon, 03 Mar 2014 12:48:20 +0100 blanchet adapted to absence of 'unfold'
Mon, 03 Mar 2014 12:48:20 +0100 blanchet got rid of automatically generated fold constant and theorems (to reduce overhead)
Mon, 03 Mar 2014 12:48:20 +0100 blanchet use same identity function for abs and rep (doesn't seem to confuse any proofs)
Mon, 03 Mar 2014 12:48:20 +0100 blanchet make 'typedef' optional, depending on size of original type
Mon, 03 Mar 2014 12:48:19 +0100 blanchet use aconv to compare terms (for cleanliness)
Mon, 03 Mar 2014 12:48:19 +0100 blanchet tuning
Mon, 03 Mar 2014 12:48:19 +0100 blanchet optimize cardinal bounds involving natLeq (omega)
Mon, 03 Mar 2014 03:13:45 +0100 wenzelm no extend_word for now, it is in conflict with manual reformatting of sources via TAB (e.g. accidental replacement of 'assume' by 'assumes');
Sun, 02 Mar 2014 22:43:20 +0100 wenzelm merged
Sun, 02 Mar 2014 22:39:34 +0100 wenzelm more standard module name;
Sun, 02 Mar 2014 22:37:55 +0100 wenzelm silence warning due to addsimps @{thms dnf_simps}: duplicate not_not rule via simp_thms and nnf_simps;
Sun, 02 Mar 2014 22:24:52 +0100 wenzelm tuned whitespace;
Sun, 02 Mar 2014 22:03:27 +0100 wenzelm allow suffix of underscores (usually unused names), to extend completion beyond already recognized entry;
Sun, 02 Mar 2014 21:52:44 +0100 wenzelm tuned proofs;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip