Tue, 03 May 2011 17:31:16 +0200 more precise source position for @{rail};
wenzelm [Tue, 03 May 2011 17:31:16 +0200] rev 42657
more precise source position for @{rail};
Tue, 03 May 2011 16:54:26 +0200 sane paragraph layout;
wenzelm [Tue, 03 May 2011 16:54:26 +0200] rev 42656
sane paragraph layout;
Tue, 03 May 2011 16:00:29 +0200 updated configuration options -- no ML here;
wenzelm [Tue, 03 May 2011 16:00:29 +0200] rev 42655
updated configuration options -- no ML here;
Tue, 03 May 2011 15:37:17 +0200 tag ML as in IsarImplementation;
wenzelm [Tue, 03 May 2011 15:37:17 +0200] rev 42654
tag ML as in IsarImplementation;
Tue, 03 May 2011 15:35:07 +0200 treat underscore as in IsarRef;
wenzelm [Tue, 03 May 2011 15:35:07 +0200] rev 42653
treat underscore as in IsarRef;
Tue, 03 May 2011 15:29:49 +0200 reactivated codegen example based on Lambda.thy;
wenzelm [Tue, 03 May 2011 15:29:49 +0200] rev 42652
reactivated codegen example based on Lambda.thy;
Tue, 03 May 2011 15:07:36 +0200 formal Base theory;
wenzelm [Tue, 03 May 2011 15:07:36 +0200] rev 42651
formal Base theory;
Tue, 03 May 2011 14:23:40 +0200 reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet [Tue, 03 May 2011 14:23:40 +0200] rev 42650
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
Tue, 03 May 2011 08:52:32 +0200 whitespace tuning
blanchet [Tue, 03 May 2011 08:52:32 +0200] rev 42649
whitespace tuning
Tue, 03 May 2011 08:52:16 +0200 make SML/NJ happiest
blanchet [Tue, 03 May 2011 08:52:16 +0200] rev 42648
make SML/NJ happiest
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip