Fri, 11 Mar 2011 15:21:13 +0100 bulwahn moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn correcting dependencies in IsaMakefile
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn renaming signatures and structures; correcting header
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn adapting Quickcheck theory after moving ML files
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn moving quickcheck_generators.ML to Quickcheck directory and renaming it random_generators.ML
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn moving exhaustive_generators.ML to Quickcheck directory
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn correcting dependencies after renaming
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn replacing naming of small by exhaustive
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn renaming smallvalue_generators.ML to exhaustive_generators.ML
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn renaming constants in Quickcheck_Exhaustive theory
Fri, 11 Mar 2011 15:21:12 +0100 bulwahn renaming Smallcheck to Quickcheck_Exhaustive
Fri, 11 Mar 2011 10:37:45 +0100 bulwahn only testing theory LSC_Examples when GHC is installed on the machine
Fri, 11 Mar 2011 10:37:43 +0100 bulwahn increasing timeout of example for counterexample generation
Fri, 11 Mar 2011 10:37:42 +0100 bulwahn adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
Fri, 11 Mar 2011 10:37:41 +0100 bulwahn adding lazysmallcheck example theory to HOL-ex session
Fri, 11 Mar 2011 10:37:40 +0100 bulwahn adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies
Fri, 11 Mar 2011 10:37:38 +0100 bulwahn replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
Fri, 11 Mar 2011 10:37:37 +0100 bulwahn changing invocation of ghc from interactive mode to compilation increases the performance of lazysmallcheck by a factor of twenty; changing Integer type to Int reduces by another 50 percent
Fri, 11 Mar 2011 10:37:37 +0100 bulwahn adding an example theory for Lazysmallcheck prototype
Fri, 11 Mar 2011 10:37:36 +0100 bulwahn adding Lazysmallcheck prototype to HOL-Library
Fri, 11 Mar 2011 10:37:35 +0100 bulwahn adding files for prototype of lazysmallcheck
Fri, 11 Mar 2011 08:58:29 +0100 bulwahn removing debug message in quickcheck's postprocessor
Fri, 11 Mar 2011 08:13:00 +0100 bulwahn fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
Fri, 11 Mar 2011 08:12:59 +0100 bulwahn renaming dest_plain_fun to dest_fun_upds and adding handling of undefined for postprocessing of quickcheck
Fri, 11 Mar 2011 08:12:58 +0100 bulwahn improving term postprocessing for counterexample presentation in quickcheck
Fri, 11 Mar 2011 08:12:55 +0100 bulwahn tuned
Wed, 09 Mar 2011 21:40:38 +0100 boehmes finished and tested Z3 proof reconstruction for injective functions;
Wed, 09 Mar 2011 10:28:01 +0100 blanchet improved formula for specialization, to prevent needless specializations -- and removed dead code
Wed, 09 Mar 2011 10:25:29 +0100 blanchet perform no arity check in debug mode so that we get to see the Kodkod problem
Fri, 04 Mar 2011 17:39:30 +0100 berghofe spark_end now joins proofs of VCs before writing *.prv file.
(0) -30000 -10000 -3000 -1000 -300 -100 -50 -30 +30 +50 +100 +300 +1000 +3000 +10000 +30000 tip