isabelle: Changelog

Mercurial Mercurial > repos > isabelle / changelog

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip

Wed, 14 Apr 2010 11:24:31 +0200 updated Thm.add_axiom/add_def;

wenzelm [Wed, 14 Apr 2010 11:24:31 +0200] rev 36134

updated Thm.add_axiom/add_def;

Wed, 14 Apr 2010 11:11:23 +0200 adapted PUBLISH_TEST for atbroy102, which only mounts /home/isatest;

wenzelm [Wed, 14 Apr 2010 11:11:23 +0200] rev 36133

adapted PUBLISH_TEST for atbroy102, which only mounts /home/isatest;

Tue, 13 Apr 2010 11:04:27 -0700 bring HOLCF/ex/Domain_Proofs.thy up to date

huffman [Tue, 13 Apr 2010 11:04:27 -0700] rev 36132

bring HOLCF/ex/Domain_Proofs.thy up to date

Tue, 13 Apr 2010 15:30:15 +0200 adapt Refute example to reflect latest soundness fix to Refute

blanchet [Tue, 13 Apr 2010 15:30:15 +0200] rev 36131

adapt Refute example to reflect latest soundness fix to Refute

Tue, 13 Apr 2010 15:16:54 +0200 commented out unsound "lfp"/"gfp" handling + fixed set output syntax;

blanchet [Tue, 13 Apr 2010 15:16:54 +0200] rev 36130

commented out unsound "lfp"/"gfp" handling + fixed set output syntax; the "lfp"/"gfp" bug can be reproduced by looking for a counterexample to lemma "(A \<union> B)^+ = A^+ \<union> B^+" Refute incorrectly finds a countermodel for cardinality 1 (the smallest counterexample requires cardinality 2).

Tue, 13 Apr 2010 14:08:58 +0200 merged

blanchet [Tue, 13 Apr 2010 14:08:58 +0200] rev 36129

merged

(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle