isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

Tue, 03 May 2011 15:29:49 +0200 reactivated codegen example based on Lambda.thy;

changeset

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;

changeset

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"

changeset

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

changeset

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

changeset

blanchet [Tue, 03 May 2011 08:52:16 +0200] rev 42648

make SML/NJ happiest

Tue, 03 May 2011 01:04:03 +0200 no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter

changeset

blanchet [Tue, 03 May 2011 01:04:03 +0200] rev 42647

no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter