Tue, 27 Oct 2009 21:53:13 +0100 blanchet fix typo in Nitpick manual
Tue, 27 Oct 2009 19:00:17 +0100 blanchet optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
Tue, 27 Oct 2009 17:53:19 +0100 blanchet clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak
Tue, 27 Oct 2009 16:52:06 +0100 blanchet renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
Tue, 10 Nov 2009 18:29:07 +0100 wenzelm eliminated some old uses of cumulative prems (!) in proof methods;
Tue, 10 Nov 2009 18:11:23 +0100 wenzelm eliminated some unused/obsolete Args.bang_facts;
Tue, 10 Nov 2009 16:04:57 +0100 wenzelm modernized structure Theory_Target;
Tue, 10 Nov 2009 15:33:35 +0100 wenzelm removed unused Quickcheck_RecFun_Simps;
Tue, 10 Nov 2009 15:32:43 +0100 wenzelm define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
Tue, 10 Nov 2009 14:38:39 +0100 wenzelm bang_facts: legacy feature;
Tue, 10 Nov 2009 14:38:06 +0100 wenzelm tuned proofs;
Tue, 10 Nov 2009 13:59:37 +0100 wenzelm removed obsolete name_of -- cf. decode;
Tue, 10 Nov 2009 13:45:11 +0100 wenzelm desymbolize: use Symbol.decode directly;
Tue, 10 Nov 2009 13:17:50 +0100 wenzelm try SAT_Examples last, to minimize impact of global side-effects;
Tue, 10 Nov 2009 13:05:35 +0100 wenzelm home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
Tue, 10 Nov 2009 09:22:55 +0000 paulson Inserted missing theory dependency
Mon, 09 Nov 2009 21:56:55 +0100 wenzelm merged
Mon, 09 Nov 2009 21:45:24 +0100 ballarin Merged.
Mon, 09 Nov 2009 21:33:22 +0100 ballarin Removed obsolete code.
Mon, 09 Nov 2009 21:43:44 +0100 wenzelm updated to official Poly/ML 5.3.0;
Mon, 09 Nov 2009 21:34:42 +0100 wenzelm switched some isatest sessions to official Poly/ML 5.3.0;
Mon, 09 Nov 2009 21:30:54 +0100 wenzelm setup for official Poly/ML 5.3.0, which is now the default;
Mon, 09 Nov 2009 20:47:39 +0100 wenzelm locale_const/target_notation: uniform use of Term.aconv_untyped;
Mon, 09 Nov 2009 19:42:33 +0100 wenzelm eliminated hard tabulators;
Mon, 09 Nov 2009 16:06:08 +0000 paulson fixed some inappropriate names
Mon, 09 Nov 2009 15:50:31 +0000 paulson merged
Mon, 09 Nov 2009 15:50:15 +0000 paulson New theory Probability/Borel.thy, and some associated lemmas
Mon, 09 Nov 2009 14:47:25 +0100 haftmann merged
Mon, 09 Nov 2009 14:47:16 +0100 haftmann tuned error messages; tuned code
Mon, 09 Nov 2009 11:34:22 +0100 boehmes follow standard theory merge behaviour: do not change already selected solver
Mon, 09 Nov 2009 11:19:25 +0100 boehmes generalized proof by abstraction,
Mon, 09 Nov 2009 08:57:07 +0100 boehmes made theory merge deterministic wrt. the selected solver
Sun, 08 Nov 2009 21:01:08 +0100 wenzelm merged
Sun, 08 Nov 2009 20:50:31 +0100 berghofe merged
Sun, 08 Nov 2009 15:45:09 +0100 berghofe Repaired handling of comprehensions in "values" command.
Sun, 08 Nov 2009 21:00:05 +0100 wenzelm updated functor Theory_Data, Proof_Data, Generic_Data;
Sun, 08 Nov 2009 19:15:37 +0100 wenzelm modernized structure Reorient_Proc;
Sun, 08 Nov 2009 18:43:42 +0100 wenzelm adapted Theory_Data;
Sun, 08 Nov 2009 18:43:22 +0100 wenzelm adapted Theory_Data;
Sun, 08 Nov 2009 18:42:57 +0100 wenzelm tuned;
Sun, 08 Nov 2009 16:30:41 +0100 wenzelm adapted Generic_Data, Proof_Data;
Sun, 08 Nov 2009 16:28:18 +0100 wenzelm adapted Generic_Data;
Sun, 08 Nov 2009 16:27:50 +0100 wenzelm modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
Sun, 08 Nov 2009 14:44:31 +0100 wenzelm added "declaration (pervasive)";
Sun, 08 Nov 2009 14:38:36 +0100 wenzelm print_theorems: suppress concealed (global) facts, unless "!" option is given;
Sun, 08 Nov 2009 13:57:07 +0100 wenzelm updated generated file;
Sun, 08 Nov 2009 13:56:44 +0100 wenzelm modernized structure Random_Word;
Sun, 08 Nov 2009 13:44:16 +0100 wenzelm init_component: slightly more robust read (raw input, succeed on non-terminated last line);
Sat, 07 Nov 2009 18:55:50 +0000 webertj merged
Sat, 07 Nov 2009 18:55:30 +0000 webertj Due to popular demand: added a function that benchmarks proof reconstruction
Sat, 07 Nov 2009 18:53:29 +0000 webertj Turned sections into subsections (better document structure).
Sat, 07 Nov 2009 08:31:56 -0800 huffman merged
Sat, 07 Nov 2009 07:37:20 -0800 huffman merged
Fri, 06 Nov 2009 09:50:37 -0800 huffman fix name of lemma snd_strict
Thu, 05 Nov 2009 15:38:09 -0800 huffman use try instead of handle
Thu, 05 Nov 2009 11:47:00 -0800 huffman map functions for various types, with ep_pair/deflation/finite_deflation lemmas
Thu, 05 Nov 2009 11:36:30 -0800 huffman lemma deflation_strict
Sat, 07 Nov 2009 16:54:13 +0100 wenzelm tuned ML_OPTIONS for SML/NJ -- for improved performance;
Sat, 07 Nov 2009 08:18:12 +0100 haftmann merged
Sat, 07 Nov 2009 08:17:53 +0100 haftmann added predicate example
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip