Wed, 11 Nov 2009 15:43:03 +0100 changed URL of SMT server,
boehmes [Wed, 11 Nov 2009 15:43:03 +0100] rev 33610
changed URL of SMT server, added Z3 rewrite lemma
Wed, 11 Nov 2009 14:04:56 +0000 Added two new lemmas
paulson [Wed, 11 Nov 2009 14:04:56 +0000] rev 33609
Added two new lemmas
Wed, 11 Nov 2009 09:02:37 +0100 tuned imports
haftmann [Wed, 11 Nov 2009 09:02:37 +0100] rev 33608
tuned imports
Wed, 11 Nov 2009 09:02:20 +0100 tuned
haftmann [Wed, 11 Nov 2009 09:02:20 +0100] rev 33607
tuned
Wed, 11 Nov 2009 00:11:26 +0100 local mutex for theory content/identity operations;
wenzelm [Wed, 11 Nov 2009 00:11:26 +0100] rev 33606
local mutex for theory content/identity operations;
Wed, 11 Nov 2009 00:09:15 +0100 admit dummy implementation;
wenzelm [Wed, 11 Nov 2009 00:09:15 +0100] rev 33605
admit dummy implementation;
Tue, 10 Nov 2009 23:18:03 +0100 Toplevel.thread provides Isar-style exception output;
wenzelm [Tue, 10 Nov 2009 23:18:03 +0100] rev 33604
Toplevel.thread provides Isar-style exception output;
Tue, 10 Nov 2009 23:15:20 +0100 generalized Runtime.toplevel_error wrt. output function;
wenzelm [Tue, 10 Nov 2009 23:15:20 +0100] rev 33603
generalized Runtime.toplevel_error wrt. output function;
Tue, 10 Nov 2009 23:15:15 +0100 exported SimpleThread.attributes;
wenzelm [Tue, 10 Nov 2009 23:15:15 +0100] rev 33602
exported SimpleThread.attributes;
Tue, 10 Nov 2009 21:28:46 +0100 plain add_preference, no setmp_CRITICAL required;
wenzelm [Tue, 10 Nov 2009 21:28:46 +0100] rev 33601
plain add_preference, no setmp_CRITICAL required;
Tue, 10 Nov 2009 21:04:30 +0100 adapted Theory_Data;
wenzelm [Tue, 10 Nov 2009 21:04:30 +0100] rev 33600
adapted Theory_Data;
Tue, 10 Nov 2009 21:02:18 +0100 recovered update from 7264824baf66, which got lost in 7264824baf66;
wenzelm [Tue, 10 Nov 2009 21:02:18 +0100] rev 33599
recovered update from 7264824baf66, which got lost in 7264824baf66;
Tue, 10 Nov 2009 18:32:41 +0100 merged
wenzelm [Tue, 10 Nov 2009 18:32:41 +0100] rev 33598
merged
Tue, 10 Nov 2009 16:12:35 +0100 merged
haftmann [Tue, 10 Nov 2009 16:12:35 +0100] rev 33597
merged
Tue, 10 Nov 2009 16:11:46 +0100 tuned header
haftmann [Tue, 10 Nov 2009 16:11:46 +0100] rev 33596
tuned header
Tue, 10 Nov 2009 16:11:43 +0100 substantial simplification restores code generation
haftmann [Tue, 10 Nov 2009 16:11:43 +0100] rev 33595
substantial simplification restores code generation
Tue, 10 Nov 2009 16:11:39 +0100 lemmas about apfst and apsnd
haftmann [Tue, 10 Nov 2009 16:11:39 +0100] rev 33594
lemmas about apfst and apsnd
Tue, 10 Nov 2009 16:11:37 +0100 tuned imports
haftmann [Tue, 10 Nov 2009 16:11:37 +0100] rev 33593
tuned imports
Tue, 10 Nov 2009 06:48:26 -0800 merged
huffman [Tue, 10 Nov 2009 06:48:26 -0800] rev 33592
merged
Tue, 10 Nov 2009 06:47:55 -0800 HOLCF example: domain package proofs done manually
huffman [Tue, 10 Nov 2009 06:47:55 -0800] rev 33591
HOLCF example: domain package proofs done manually
Tue, 10 Nov 2009 06:30:19 -0800 add lemma parallel_fix_ind
huffman [Tue, 10 Nov 2009 06:30:19 -0800] rev 33590
add lemma parallel_fix_ind
Tue, 10 Nov 2009 06:30:08 -0800 add title/author block
huffman [Tue, 10 Nov 2009 06:30:08 -0800] rev 33589
add title/author block
Tue, 10 Nov 2009 06:22:29 -0800 theory of representable cpos
huffman [Tue, 10 Nov 2009 06:22:29 -0800] rev 33588
theory of representable cpos
Mon, 09 Nov 2009 15:51:32 -0800 add map_map lemmas
huffman [Mon, 09 Nov 2009 15:51:32 -0800] rev 33587
add map_map lemmas
Mon, 09 Nov 2009 15:29:58 -0800 add in_deflation relation, more lemmas about cast
huffman [Mon, 09 Nov 2009 15:29:58 -0800] rev 33586
add in_deflation relation, more lemmas about cast
Mon, 09 Nov 2009 12:40:47 -0800 ep_pair and deflation lemmas for powerdomain map functions
huffman [Mon, 09 Nov 2009 12:40:47 -0800] rev 33585
ep_pair and deflation lemmas for powerdomain map functions
Tue, 10 Nov 2009 14:20:15 +0100 remove spurious parameter to "merge"
blanchet [Tue, 10 Nov 2009 14:20:15 +0100] rev 33584
remove spurious parameter to "merge"
Tue, 10 Nov 2009 13:54:00 +0100 merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
blanchet [Tue, 10 Nov 2009 13:54:00 +0100] rev 33583
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
Tue, 10 Nov 2009 13:46:40 +0100 fixed soundness bug in Nitpick related to sets of sets;
blanchet [Tue, 10 Nov 2009 13:46:40 +0100] rev 33582
fixed soundness bug in Nitpick related to sets of sets; (detected thanks to the TPTP)
Thu, 05 Nov 2009 19:06:35 +0100 added possibility to register datatypes as codatatypes in Nitpick;
blanchet [Thu, 05 Nov 2009 19:06:35 +0100] rev 33581
added possibility to register datatypes as codatatypes in Nitpick; this is useful if the datatype is used only as a means to define the codatatype
Thu, 05 Nov 2009 17:03:22 +0100 added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
blanchet [Thu, 05 Nov 2009 17:03:22 +0100] rev 33580
added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes
Thu, 05 Nov 2009 17:00:28 +0100 don't promise too much in the Nitpick manual
blanchet [Thu, 05 Nov 2009 17:00:28 +0100] rev 33579
don't promise too much in the Nitpick manual
Thu, 05 Nov 2009 11:58:36 +0100 merged
blanchet [Thu, 05 Nov 2009 11:58:36 +0100] rev 33578
merged
Thu, 05 Nov 2009 11:58:07 +0100 added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package;
blanchet [Thu, 05 Nov 2009 11:58:07 +0100] rev 33577
added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package; this ensures that Nitpick can find the definition and determine whether its inductive or coinductive
Thu, 29 Oct 2009 23:08:51 +0100 merged
blanchet [Thu, 29 Oct 2009 23:08:51 +0100] rev 33576
merged
Thu, 29 Oct 2009 22:31:30 +0100 try very hard to remove temporary files generated by Nitpick in case of interruption
blanchet [Thu, 29 Oct 2009 22:31:30 +0100] rev 33575
try very hard to remove temporary files generated by Nitpick in case of interruption
Thu, 29 Oct 2009 21:57:59 +0100 eliminate two FIXMEs in Nitpick's monotonicity check code
blanchet [Thu, 29 Oct 2009 21:57:59 +0100] rev 33574
eliminate two FIXMEs in Nitpick's monotonicity check code
Thu, 29 Oct 2009 16:06:28 +0100 rename "NitpickMono" to "Nitpick_Mono" in example
blanchet [Thu, 29 Oct 2009 16:06:28 +0100] rev 33573
rename "NitpickMono" to "Nitpick_Mono" in example
Thu, 29 Oct 2009 15:26:00 +0100 merged
blanchet [Thu, 29 Oct 2009 15:26:00 +0100] rev 33572
merged
Thu, 29 Oct 2009 15:24:52 +0100 minor cleanup in Nitpick
blanchet [Thu, 29 Oct 2009 15:24:52 +0100] rev 33571
minor cleanup in Nitpick
Thu, 29 Oct 2009 15:23:25 +0100 make "auto" SAT solver less verbose
blanchet [Thu, 29 Oct 2009 15:23:25 +0100] rev 33570
make "auto" SAT solver less verbose
Thu, 29 Oct 2009 15:16:54 +0100 make "sizechange_tac" slightly less verbose
blanchet [Thu, 29 Oct 2009 15:16:54 +0100] rev 33569
make "sizechange_tac" slightly less verbose
Thu, 29 Oct 2009 12:50:44 +0100 don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
blanchet [Thu, 29 Oct 2009 12:50:44 +0100] rev 33568
don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)
Thu, 29 Oct 2009 12:29:31 +0100 readded Predicate_Compile to Main
blanchet [Thu, 29 Oct 2009 12:29:31 +0100] rev 33567
readded Predicate_Compile to Main
Thu, 29 Oct 2009 12:09:32 +0100 merged
blanchet [Thu, 29 Oct 2009 12:09:32 +0100] rev 33566
merged
Thu, 29 Oct 2009 11:41:37 +0100 fixed error in Nitpick's display of uncurried constants, which resulted in an exception
blanchet [Thu, 29 Oct 2009 11:41:37 +0100] rev 33565
fixed error in Nitpick's display of uncurried constants, which resulted in an exception
Thu, 29 Oct 2009 11:41:11 +0100 fixed minor problems with Nitpick's documentation
blanchet [Thu, 29 Oct 2009 11:41:11 +0100] rev 33564
fixed minor problems with Nitpick's documentation
Wed, 28 Oct 2009 18:21:13 +0100 merged
blanchet [Wed, 28 Oct 2009 18:21:13 +0100] rev 33563
merged
Wed, 28 Oct 2009 18:09:30 +0100 merged my Auto Nitpick change with Lukas's Predicate Compiler changes
blanchet [Wed, 28 Oct 2009 18:09:30 +0100] rev 33562
merged my Auto Nitpick change with Lukas's Predicate Compiler changes
Wed, 28 Oct 2009 17:43:43 +0100 introduced Auto Nitpick in addition to Auto Quickcheck;
blanchet [Wed, 28 Oct 2009 17:43:43 +0100] rev 33561
introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian
Wed, 28 Oct 2009 11:55:48 +0100 use "get_goal" rather than "flat_goal" in Auto Quickcheck, since we don't need the extra facts for counterexample generation
blanchet [Wed, 28 Oct 2009 11:55:48 +0100] rev 33560
use "get_goal" rather than "flat_goal" in Auto Quickcheck, since we don't need the extra facts for counterexample generation
Tue, 27 Oct 2009 21:53:13 +0100 fix typo in Nitpick manual
blanchet [Tue, 27 Oct 2009 21:53:13 +0100] rev 33559
fix typo in Nitpick manual
Tue, 27 Oct 2009 19:00:17 +0100 optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
blanchet [Tue, 27 Oct 2009 19:00:17 +0100] rev 33558
optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem
Tue, 27 Oct 2009 17:53:19 +0100 clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak
blanchet [Tue, 27 Oct 2009 17:53:19 +0100] rev 33557
clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak
Tue, 27 Oct 2009 16:52:06 +0100 renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
blanchet [Tue, 27 Oct 2009 16:52:06 +0100] rev 33556
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 eliminated some old uses of cumulative prems (!) in proof methods;
wenzelm [Tue, 10 Nov 2009 18:29:07 +0100] rev 33555
eliminated some old uses of cumulative prems (!) in proof methods;
Tue, 10 Nov 2009 18:11:23 +0100 eliminated some unused/obsolete Args.bang_facts;
wenzelm [Tue, 10 Nov 2009 18:11:23 +0100] rev 33554
eliminated some unused/obsolete Args.bang_facts;
Tue, 10 Nov 2009 16:04:57 +0100 modernized structure Theory_Target;
wenzelm [Tue, 10 Nov 2009 16:04:57 +0100] rev 33553
modernized structure Theory_Target;
Tue, 10 Nov 2009 15:33:35 +0100 removed unused Quickcheck_RecFun_Simps;
wenzelm [Tue, 10 Nov 2009 15:33:35 +0100] rev 33552
removed unused Quickcheck_RecFun_Simps;
Tue, 10 Nov 2009 15:32:43 +0100 define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
wenzelm [Tue, 10 Nov 2009 15:32:43 +0100] rev 33551
define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
Tue, 10 Nov 2009 14:38:39 +0100 bang_facts: legacy feature;
wenzelm [Tue, 10 Nov 2009 14:38:39 +0100] rev 33550
bang_facts: legacy feature;
Tue, 10 Nov 2009 14:38:06 +0100 tuned proofs;
wenzelm [Tue, 10 Nov 2009 14:38:06 +0100] rev 33549
tuned proofs;
Tue, 10 Nov 2009 13:59:37 +0100 removed obsolete name_of -- cf. decode;
wenzelm [Tue, 10 Nov 2009 13:59:37 +0100] rev 33548
removed obsolete name_of -- cf. decode;
Tue, 10 Nov 2009 13:45:11 +0100 desymbolize: use Symbol.decode directly;
wenzelm [Tue, 10 Nov 2009 13:45:11 +0100] rev 33547
desymbolize: use Symbol.decode directly; recovered coding conventions of this file;
Tue, 10 Nov 2009 13:17:50 +0100 try SAT_Examples last, to minimize impact of global side-effects;
wenzelm [Tue, 10 Nov 2009 13:17:50 +0100] rev 33546
try SAT_Examples last, to minimize impact of global side-effects;
Tue, 10 Nov 2009 13:05:35 +0100 home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);
wenzelm [Tue, 10 Nov 2009 13:05:35 +0100] rev 33545
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 Inserted missing theory dependency
paulson [Tue, 10 Nov 2009 09:22:55 +0000] rev 33544
Inserted missing theory dependency
Mon, 09 Nov 2009 21:56:55 +0100 merged
wenzelm [Mon, 09 Nov 2009 21:56:55 +0100] rev 33543
merged
Mon, 09 Nov 2009 21:45:24 +0100 Merged.
ballarin [Mon, 09 Nov 2009 21:45:24 +0100] rev 33542
Merged.
Mon, 09 Nov 2009 21:33:22 +0100 Removed obsolete code.
ballarin [Mon, 09 Nov 2009 21:33:22 +0100] rev 33541
Removed obsolete code.
Mon, 09 Nov 2009 21:43:44 +0100 updated to official Poly/ML 5.3.0;
wenzelm [Mon, 09 Nov 2009 21:43:44 +0100] rev 33540
updated to official Poly/ML 5.3.0;
Mon, 09 Nov 2009 21:34:42 +0100 switched some isatest sessions to official Poly/ML 5.3.0;
wenzelm [Mon, 09 Nov 2009 21:34:42 +0100] rev 33539
switched some isatest sessions to official Poly/ML 5.3.0;
Mon, 09 Nov 2009 21:30:54 +0100 setup for official Poly/ML 5.3.0, which is now the default;
wenzelm [Mon, 09 Nov 2009 21:30:54 +0100] rev 33538
setup for official Poly/ML 5.3.0, which is now the default;
Mon, 09 Nov 2009 20:47:39 +0100 locale_const/target_notation: uniform use of Term.aconv_untyped;
wenzelm [Mon, 09 Nov 2009 20:47:39 +0100] rev 33537
locale_const/target_notation: uniform use of Term.aconv_untyped; target_notation: pass on transformed term formally; removed obsolete Type.similar_types;
Mon, 09 Nov 2009 19:42:33 +0100 eliminated hard tabulators;
wenzelm [Mon, 09 Nov 2009 19:42:33 +0100] rev 33536
eliminated hard tabulators;
Mon, 09 Nov 2009 16:06:08 +0000 fixed some inappropriate names
paulson [Mon, 09 Nov 2009 16:06:08 +0000] rev 33535
fixed some inappropriate names
Mon, 09 Nov 2009 15:50:31 +0000 merged
paulson [Mon, 09 Nov 2009 15:50:31 +0000] rev 33534
merged
Mon, 09 Nov 2009 15:50:15 +0000 New theory Probability/Borel.thy, and some associated lemmas
paulson [Mon, 09 Nov 2009 15:50:15 +0000] rev 33533
New theory Probability/Borel.thy, and some associated lemmas
Mon, 09 Nov 2009 14:47:25 +0100 merged
haftmann [Mon, 09 Nov 2009 14:47:25 +0100] rev 33532
merged
Mon, 09 Nov 2009 14:47:16 +0100 tuned error messages; tuned code
haftmann [Mon, 09 Nov 2009 14:47:16 +0100] rev 33531
tuned error messages; tuned code
Mon, 09 Nov 2009 11:34:22 +0100 follow standard theory merge behaviour: do not change already selected solver
boehmes [Mon, 09 Nov 2009 11:34:22 +0100] rev 33530
follow standard theory merge behaviour: do not change already selected solver
Mon, 09 Nov 2009 11:19:25 +0100 generalized proof by abstraction,
boehmes [Mon, 09 Nov 2009 11:19:25 +0100] rev 33529
generalized proof by abstraction, abstract propositional nnf goals (lets best_tac succeed on very large terms)
Mon, 09 Nov 2009 08:57:07 +0100 made theory merge deterministic wrt. the selected solver
boehmes [Mon, 09 Nov 2009 08:57:07 +0100] rev 33528
made theory merge deterministic wrt. the selected solver
Sun, 08 Nov 2009 21:01:08 +0100 merged
wenzelm [Sun, 08 Nov 2009 21:01:08 +0100] rev 33527
merged
Sun, 08 Nov 2009 20:50:31 +0100 merged
berghofe [Sun, 08 Nov 2009 20:50:31 +0100] rev 33526
merged
Sun, 08 Nov 2009 15:45:09 +0100 Repaired handling of comprehensions in "values" command.
berghofe [Sun, 08 Nov 2009 15:45:09 +0100] rev 33525
Repaired handling of comprehensions in "values" command.
Sun, 08 Nov 2009 21:00:05 +0100 updated functor Theory_Data, Proof_Data, Generic_Data;
wenzelm [Sun, 08 Nov 2009 21:00:05 +0100] rev 33524
updated functor Theory_Data, Proof_Data, Generic_Data;
Sun, 08 Nov 2009 19:15:37 +0100 modernized structure Reorient_Proc;
wenzelm [Sun, 08 Nov 2009 19:15:37 +0100] rev 33523
modernized structure Reorient_Proc; explicit merge of constituent functions, avoids exponential blowup when traversing the import graph; adapted Theory_Data; tuned;
Sun, 08 Nov 2009 18:43:42 +0100 adapted Theory_Data;
wenzelm [Sun, 08 Nov 2009 18:43:42 +0100] rev 33522
adapted Theory_Data; tuned;
Sun, 08 Nov 2009 18:43:22 +0100 adapted Theory_Data;
wenzelm [Sun, 08 Nov 2009 18:43:22 +0100] rev 33521
adapted Theory_Data; handle Symtab.DUP during actual merge;
Sun, 08 Nov 2009 18:42:57 +0100 tuned;
wenzelm [Sun, 08 Nov 2009 18:42:57 +0100] rev 33520
tuned;
Sun, 08 Nov 2009 16:30:41 +0100 adapted Generic_Data, Proof_Data;
wenzelm [Sun, 08 Nov 2009 16:30:41 +0100] rev 33519
adapted Generic_Data, Proof_Data; tuned;
Sun, 08 Nov 2009 16:28:18 +0100 adapted Generic_Data;
wenzelm [Sun, 08 Nov 2009 16:28:18 +0100] rev 33518
adapted Generic_Data; proper merge of fst/fst and snd/snd;
Sun, 08 Nov 2009 16:27:50 +0100 modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
wenzelm [Sun, 08 Nov 2009 16:27:50 +0100] rev 33517
modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;
Sun, 08 Nov 2009 14:44:31 +0100 added "declaration (pervasive)";
wenzelm [Sun, 08 Nov 2009 14:44:31 +0100] rev 33516
added "declaration (pervasive)";
Sun, 08 Nov 2009 14:38:36 +0100 print_theorems: suppress concealed (global) facts, unless "!" option is given;
wenzelm [Sun, 08 Nov 2009 14:38:36 +0100] rev 33515
print_theorems: suppress concealed (global) facts, unless "!" option is given;
(0) -30000 -10000 -3000 -1000 -300 -100 -96 +96 +100 +300 +1000 +3000 +10000 +30000 tip