blanchet [Tue, 03 May 2011 18:47:22 +0200] rev 42659
fixed long name truncation logic
wenzelm [Tue, 03 May 2011 18:04:05 +0200] rev 42658
some documentation of @{rail} antiquotation;
wenzelm [Tue, 03 May 2011 17:31:16 +0200] rev 42657
more precise source position for @{rail};
wenzelm [Tue, 03 May 2011 16:54:26 +0200] rev 42656
sane paragraph layout;
wenzelm [Tue, 03 May 2011 16:00:29 +0200] rev 42655
updated configuration options -- no ML here;
wenzelm [Tue, 03 May 2011 15:37:17 +0200] rev 42654
tag ML as in IsarImplementation;
wenzelm [Tue, 03 May 2011 15:35:07 +0200] rev 42653
treat underscore as in IsarRef;
wenzelm [Tue, 03 May 2011 15:29:49 +0200] rev 42652
reactivated codegen example based on Lambda.thy;
wenzelm [Tue, 03 May 2011 15:07:36 +0200] rev 42651
formal Base theory;
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"