wenzelm [Thu, 13 Feb 2014 12:09:51 +0100] rev 55448
explicit indication that redefining outer syntax commands is not supposed to happen -- NB: interactive mode requires global change of syntax;
wenzelm [Thu, 13 Feb 2014 11:54:14 +0100] rev 55447
do not redefine outer syntax commands;
wenzelm [Thu, 13 Feb 2014 11:37:00 +0100] rev 55446
tuned whitespace;
wenzelm [Thu, 13 Feb 2014 11:23:55 +0100] rev 55445
static repair of ML file -- untested (!) by default since 76965c356d2a;
blanchet [Wed, 12 Feb 2014 17:36:00 +0100] rev 55444
iteration n in the 'default' vs. 'update_new' vs. 'update' saga -- 'update' makes sense now that we honor the canonical order on 'merge' (as opposed to raising 'DUP')
blanchet [Wed, 12 Feb 2014 17:35:59 +0100] rev 55443
don't hide constant forever, since it may appear in some 'primcorec'-generated theorems
blanchet [Wed, 12 Feb 2014 17:35:59 +0100] rev 55442
tuning
traytel [Wed, 12 Feb 2014 16:35:58 +0100] rev 55441
HOL-IMP fastness
wenzelm [Wed, 12 Feb 2014 14:32:45 +0100] rev 55440
merged, resolving some conflicts;
wenzelm [Wed, 12 Feb 2014 13:56:43 +0100] rev 55439
eliminated hard tabs (assuming tab-width=2);
wenzelm [Wed, 12 Feb 2014 13:53:11 +0100] rev 55438
more platform notes;
wenzelm [Wed, 12 Feb 2014 13:33:05 +0100] rev 55437
tuned whitespace;
wenzelm [Wed, 12 Feb 2014 13:31:18 +0100] rev 55436
removed odd comments -- inferred types are shown by Prover IDE;
wenzelm [Wed, 12 Feb 2014 11:28:17 +0100] rev 55435
maintain blob edits within history, which is important for Snapshot.convert/revert;
wenzelm [Wed, 12 Feb 2014 11:05:48 +0100] rev 55434
more accurate eq_content;