Sun, 13 Mar 2011 15:13:53 +0100 wenzelm isatest: test more external code;
Sun, 13 Mar 2011 15:10:00 +0100 wenzelm tuned headers;
Sun, 13 Mar 2011 14:51:38 +0100 wenzelm allow spaces in executable names;
Sun, 13 Mar 2011 13:57:20 +0100 wenzelm tuned;
Sun, 13 Mar 2011 13:53:54 +0100 wenzelm tuned headers;
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn adapting example file to renaming of the quickcheck tester
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn renaming tester from lazy_exhaustive to narrowing
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn renaming example file correctly
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn adapting Main file generation for Quickcheck_Narrowing
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn adapting Quickcheck_Narrowing and example file to new names
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn renaming LSC_Examples theory to Quickcheck_Narrowing
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn renaming lazysmallcheck ML file to Quickcheck_Narrowing
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn renaming LSC to Quickcheck_Narrowing
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn adaptions in generators using the common functions
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn adding file quickcheck_common to carry common functions of all quickcheck generators
Fri, 11 Mar 2011 15:21:13 +0100 bulwahn adapting record package to renaming of quickcheck's structures
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.
Fri, 04 Mar 2011 11:43:20 +0100 krauss clarified
Fri, 04 Mar 2011 11:52:54 +0100 krauss produce helpful mira summary for more errors
Fri, 04 Mar 2011 00:09:47 +0100 wenzelm eliminated prems;
Thu, 03 Mar 2011 22:06:15 +0100 wenzelm eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
Thu, 03 Mar 2011 21:43:06 +0100 wenzelm tuned proofs -- eliminated prems;
Thu, 03 Mar 2011 18:43:15 +0100 wenzelm merged
Thu, 03 Mar 2011 14:38:31 +0100 blanchet merged
Thu, 03 Mar 2011 14:25:15 +0100 blanchet don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
Thu, 03 Mar 2011 18:42:12 +0100 wenzelm simplified Thy_Info.check_file -- discontinued load path;
Thu, 03 Mar 2011 18:10:28 +0100 wenzelm discontinued legacy load path;
Thu, 03 Mar 2011 15:56:17 +0100 wenzelm re-interpret ProofGeneralPgip.changecwd as Thy_Load.set_master_path, presuming that this is close to the intended semantics;
Thu, 03 Mar 2011 15:46:02 +0100 wenzelm modernized imports;
Thu, 03 Mar 2011 15:36:54 +0100 wenzelm observe standard header format;
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip