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;
Sun, 02 Mar 2014 21:30:47 +0100 wenzelm prefer Name_Space.check with its builtin reports (including completion);
Sun, 02 Mar 2014 21:13:29 +0100 wenzelm tuned source structure;
Sun, 02 Mar 2014 21:02:27 +0100 wenzelm prefer Name_Space.check with its builtin reports (including completion);
Sun, 02 Mar 2014 20:34:11 +0100 wenzelm consider completion report as part of error message -- less stateful, may get handled;
Sun, 02 Mar 2014 20:20:20 +0100 wenzelm more markup for read_class: imitate Name_Space.check despite lack of Name_Space.table;
Sun, 02 Mar 2014 19:45:38 +0100 wenzelm more antiquotations;
Sun, 02 Mar 2014 19:00:45 +0100 wenzelm clarified names of antiquotations and markup;
Sun, 02 Mar 2014 19:15:23 +0100 nipkow tuned proof
Sun, 02 Mar 2014 18:41:41 +0100 nipkow merged
Sun, 02 Mar 2014 18:41:26 +0100 nipkow tuned proofs
Sun, 02 Mar 2014 18:20:08 +0100 wenzelm repaired document;
Sun, 02 Mar 2014 18:11:30 +0100 wenzelm repaired document;
Sun, 02 Mar 2014 00:05:35 +0100 wenzelm more markup for ML source;
Sat, 01 Mar 2014 23:48:55 +0100 wenzelm merged
Sat, 01 Mar 2014 23:17:37 +0100 wenzelm tuned signature;
Sat, 01 Mar 2014 22:46:31 +0100 wenzelm clarified language markup: added "delimited" property;
Sat, 01 Mar 2014 19:55:01 +0100 wenzelm clarified module structure;
Sat, 01 Mar 2014 19:43:35 +0100 wenzelm tuned;
Sat, 01 Mar 2014 19:39:27 +0100 wenzelm tuned signature -- separate module Font_Info;
Sat, 01 Mar 2014 18:33:49 +0100 wenzelm tuned;
Sat, 01 Mar 2014 16:34:30 +0100 wenzelm font size change with delay, to avoid GUI lagging behind user input;
Sat, 01 Mar 2014 15:58:47 +0100 wenzelm incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
Sat, 01 Mar 2014 13:05:46 +0100 wenzelm more symbols, less parentheses;
Sat, 01 Mar 2014 12:07:26 +0100 wenzelm tuned signature -- more explicit Document.Elements;
Sat, 01 Mar 2014 20:40:31 +0100 traytel made SML/NJ happier
Sat, 01 Mar 2014 17:08:39 +0100 haftmann more precise imports;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 tip