Wed, 05 Mar 2014 19:52:28 +0100 wenzelm tuned;
Wed, 05 Mar 2014 18:26:35 +0100 wenzelm more markup for inner syntax class/type names (notably for completion);
Wed, 05 Mar 2014 17:36:40 +0100 wenzelm tuned proofs;
Wed, 05 Mar 2014 16:16:36 +0100 wenzelm back to stable polyml-5.5.1, due to problems with Poly/ML SVN 1913 and HOL-Proofs (Fail "Insufficient memory");
Wed, 05 Mar 2014 16:13:24 +0100 wenzelm more explicit quasi_keyword markup, for Args.$$$ material, which is somewhere in between of outer and inner syntax;
Wed, 05 Mar 2014 16:06:11 +0100 wenzelm unused;
Wed, 05 Mar 2014 15:25:52 +0100 wenzelm special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
Wed, 05 Mar 2014 15:24:06 +0100 wenzelm more thorough (potentially duplicate) markup, e.g. relevant for embedded Args syntax within antiquotations;
Wed, 05 Mar 2014 14:19:54 +0100 wenzelm suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
Wed, 05 Mar 2014 13:11:08 +0100 wenzelm clarified init_assignable: make double-sure that initial values are reset;
Wed, 05 Mar 2014 09:59:48 +0100 wenzelm proper UTF-8;
Tue, 04 Mar 2014 16:16:05 -0800 huffman fix typo
Tue, 04 Mar 2014 15:26:12 -0800 huffman remove simp rules made redundant by the replacement of neg_numeral with negated numerals
Tue, 04 Mar 2014 14:14:28 -0800 huffman tuned proof
Tue, 04 Mar 2014 14:00:59 -0800 huffman tuned proof script
Tue, 04 Mar 2014 22:30:12 +0100 blanchet no 'sorry' so that the schematic variable gets instantiated
Tue, 04 Mar 2014 21:42:40 +0100 blanchet removed junk
Tue, 04 Mar 2014 18:57:17 +0100 blanchet simplify sets in BNF composition
Tue, 04 Mar 2014 18:57:17 +0100 blanchet tuning
Tue, 04 Mar 2014 18:57:17 +0100 blanchet more caching in composition pipeline
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
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip