boehmes [Wed, 11 Nov 2009 15:43:03 +0100] rev 33610
changed URL of SMT server,
added Z3 rewrite lemma
paulson [Wed, 11 Nov 2009 14:04:56 +0000] rev 33609
Added two new lemmas
haftmann [Wed, 11 Nov 2009 09:02:37 +0100] rev 33608
tuned imports
haftmann [Wed, 11 Nov 2009 09:02:20 +0100] rev 33607
tuned
wenzelm [Wed, 11 Nov 2009 00:11:26 +0100] rev 33606
local mutex for theory content/identity operations;
wenzelm [Wed, 11 Nov 2009 00:09:15 +0100] rev 33605
admit dummy implementation;
wenzelm [Tue, 10 Nov 2009 23:18:03 +0100] rev 33604
Toplevel.thread provides Isar-style exception output;
wenzelm [Tue, 10 Nov 2009 23:15:20 +0100] rev 33603
generalized Runtime.toplevel_error wrt. output function;
wenzelm [Tue, 10 Nov 2009 23:15:15 +0100] rev 33602
exported SimpleThread.attributes;
wenzelm [Tue, 10 Nov 2009 21:28:46 +0100] rev 33601
plain add_preference, no setmp_CRITICAL required;
wenzelm [Tue, 10 Nov 2009 21:04:30 +0100] rev 33600
adapted Theory_Data;
wenzelm [Tue, 10 Nov 2009 21:02:18 +0100] rev 33599
recovered update from 7264824baf66, which got lost in 7264824baf66;
wenzelm [Tue, 10 Nov 2009 18:32:41 +0100] rev 33598
merged
haftmann [Tue, 10 Nov 2009 16:12:35 +0100] rev 33597
merged
haftmann [Tue, 10 Nov 2009 16:11:46 +0100] rev 33596
tuned header
haftmann [Tue, 10 Nov 2009 16:11:43 +0100] rev 33595
substantial simplification restores code generation
haftmann [Tue, 10 Nov 2009 16:11:39 +0100] rev 33594
lemmas about apfst and apsnd
haftmann [Tue, 10 Nov 2009 16:11:37 +0100] rev 33593
tuned imports
huffman [Tue, 10 Nov 2009 06:48:26 -0800] rev 33592
merged
huffman [Tue, 10 Nov 2009 06:47:55 -0800] rev 33591
HOLCF example: domain package proofs done manually
huffman [Tue, 10 Nov 2009 06:30:19 -0800] rev 33590
add lemma parallel_fix_ind
huffman [Tue, 10 Nov 2009 06:30:08 -0800] rev 33589
add title/author block
huffman [Tue, 10 Nov 2009 06:22:29 -0800] rev 33588
theory of representable cpos
huffman [Mon, 09 Nov 2009 15:51:32 -0800] rev 33587
add map_map lemmas
huffman [Mon, 09 Nov 2009 15:29:58 -0800] rev 33586
add in_deflation relation, more lemmas about cast
huffman [Mon, 09 Nov 2009 12:40:47 -0800] rev 33585
ep_pair and deflation lemmas for powerdomain map functions
blanchet [Tue, 10 Nov 2009 14:20:15 +0100] rev 33584
remove spurious parameter to "merge"
blanchet [Tue, 10 Nov 2009 13:54:00 +0100] rev 33583
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
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)
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
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
blanchet [Thu, 05 Nov 2009 17:00:28 +0100] rev 33579
don't promise too much in the Nitpick manual
blanchet [Thu, 05 Nov 2009 11:58:36 +0100] rev 33578
merged
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
blanchet [Thu, 29 Oct 2009 23:08:51 +0100] rev 33576
merged
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
blanchet [Thu, 29 Oct 2009 21:57:59 +0100] rev 33574
eliminate two FIXMEs in Nitpick's monotonicity check code
blanchet [Thu, 29 Oct 2009 16:06:28 +0100] rev 33573
rename "NitpickMono" to "Nitpick_Mono" in example
blanchet [Thu, 29 Oct 2009 15:26:00 +0100] rev 33572
merged
blanchet [Thu, 29 Oct 2009 15:24:52 +0100] rev 33571
minor cleanup in Nitpick
blanchet [Thu, 29 Oct 2009 15:23:25 +0100] rev 33570
make "auto" SAT solver less verbose
blanchet [Thu, 29 Oct 2009 15:16:54 +0100] rev 33569
make "sizechange_tac" slightly less verbose
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)
blanchet [Thu, 29 Oct 2009 12:29:31 +0100] rev 33567
readded Predicate_Compile to Main
blanchet [Thu, 29 Oct 2009 12:09:32 +0100] rev 33566
merged
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
blanchet [Thu, 29 Oct 2009 11:41:11 +0100] rev 33564
fixed minor problems with Nitpick's documentation
blanchet [Wed, 28 Oct 2009 18:21:13 +0100] rev 33563
merged
blanchet [Wed, 28 Oct 2009 18:09:30 +0100] rev 33562
merged my Auto Nitpick change with Lukas's Predicate Compiler changes
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
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
blanchet [Tue, 27 Oct 2009 21:53:13 +0100] rev 33559
fix typo in Nitpick manual
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
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
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
wenzelm [Tue, 10 Nov 2009 18:29:07 +0100] rev 33555
eliminated some old uses of cumulative prems (!) in proof methods;
wenzelm [Tue, 10 Nov 2009 18:11:23 +0100] rev 33554
eliminated some unused/obsolete Args.bang_facts;
wenzelm [Tue, 10 Nov 2009 16:04:57 +0100] rev 33553
modernized structure Theory_Target;
wenzelm [Tue, 10 Nov 2009 15:33:35 +0100] rev 33552
removed unused Quickcheck_RecFun_Simps;
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;
wenzelm [Tue, 10 Nov 2009 14:38:39 +0100] rev 33550
bang_facts: legacy feature;
wenzelm [Tue, 10 Nov 2009 14:38:06 +0100] rev 33549
tuned proofs;
wenzelm [Tue, 10 Nov 2009 13:59:37 +0100] rev 33548
removed obsolete name_of -- cf. decode;
wenzelm [Tue, 10 Nov 2009 13:45:11 +0100] rev 33547
desymbolize: use Symbol.decode directly;
recovered coding conventions of this file;
wenzelm [Tue, 10 Nov 2009 13:17:50 +0100] rev 33546
try SAT_Examples last, to minimize impact of global side-effects;
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 $);
paulson [Tue, 10 Nov 2009 09:22:55 +0000] rev 33544
Inserted missing theory dependency
wenzelm [Mon, 09 Nov 2009 21:56:55 +0100] rev 33543
merged
ballarin [Mon, 09 Nov 2009 21:45:24 +0100] rev 33542
Merged.
ballarin [Mon, 09 Nov 2009 21:33:22 +0100] rev 33541
Removed obsolete code.
wenzelm [Mon, 09 Nov 2009 21:43:44 +0100] rev 33540
updated 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;
wenzelm [Mon, 09 Nov 2009 21:30:54 +0100] rev 33538
setup for official Poly/ML 5.3.0, which is now the default;
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;
wenzelm [Mon, 09 Nov 2009 19:42:33 +0100] rev 33536
eliminated hard tabulators;
paulson [Mon, 09 Nov 2009 16:06:08 +0000] rev 33535
fixed some inappropriate names
paulson [Mon, 09 Nov 2009 15:50:31 +0000] rev 33534
merged
paulson [Mon, 09 Nov 2009 15:50:15 +0000] rev 33533
New theory Probability/Borel.thy, and some associated lemmas
haftmann [Mon, 09 Nov 2009 14:47:25 +0100] rev 33532
merged
haftmann [Mon, 09 Nov 2009 14:47:16 +0100] rev 33531
tuned error messages; tuned code
boehmes [Mon, 09 Nov 2009 11:34:22 +0100] rev 33530
follow standard theory merge behaviour: do not change already selected solver
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)
boehmes [Mon, 09 Nov 2009 08:57:07 +0100] rev 33528
made theory merge deterministic wrt. the selected solver
wenzelm [Sun, 08 Nov 2009 21:01:08 +0100] rev 33527
merged
berghofe [Sun, 08 Nov 2009 20:50:31 +0100] rev 33526
merged
berghofe [Sun, 08 Nov 2009 15:45:09 +0100] rev 33525
Repaired handling of comprehensions in "values" command.
wenzelm [Sun, 08 Nov 2009 21:00:05 +0100] rev 33524
updated functor Theory_Data, Proof_Data, Generic_Data;
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;
wenzelm [Sun, 08 Nov 2009 18:43:42 +0100] rev 33522
adapted Theory_Data;
tuned;
wenzelm [Sun, 08 Nov 2009 18:43:22 +0100] rev 33521
adapted Theory_Data;
handle Symtab.DUP during actual merge;
wenzelm [Sun, 08 Nov 2009 18:42:57 +0100] rev 33520
tuned;
wenzelm [Sun, 08 Nov 2009 16:30:41 +0100] rev 33519
adapted Generic_Data, Proof_Data;
tuned;
wenzelm [Sun, 08 Nov 2009 16:28:18 +0100] rev 33518
adapted Generic_Data;
proper merge of fst/fst and snd/snd;
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;
wenzelm [Sun, 08 Nov 2009 14:44:31 +0100] rev 33516
added "declaration (pervasive)";
wenzelm [Sun, 08 Nov 2009 14:38:36 +0100] rev 33515
print_theorems: suppress concealed (global) facts, unless "!" option is given;