Sun, 13 Mar 2011 16:38:14 +0100 prefer qualified ISABELLE_NEOS_SERVER;
wenzelm [Sun, 13 Mar 2011 16:38:14 +0100] rev 41947
prefer qualified ISABELLE_NEOS_SERVER;
Sun, 13 Mar 2011 16:30:02 +0100 proper File.shell_path;
wenzelm [Sun, 13 Mar 2011 16:30:02 +0100] rev 41946
proper File.shell_path;
Sun, 13 Mar 2011 16:14:14 +0100 more conventional variable name;
wenzelm [Sun, 13 Mar 2011 16:14:14 +0100] rev 41945
more conventional variable name;
Sun, 13 Mar 2011 16:01:00 +0100 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
wenzelm [Sun, 13 Mar 2011 16:01:00 +0100] rev 41944
Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
Sun, 13 Mar 2011 15:16:37 +0100 fixed document;
wenzelm [Sun, 13 Mar 2011 15:16:37 +0100] rev 41943
fixed document;
Sun, 13 Mar 2011 15:13:53 +0100 isatest: test more external code;
wenzelm [Sun, 13 Mar 2011 15:13:53 +0100] rev 41942
isatest: test more external code;
Sun, 13 Mar 2011 15:10:00 +0100 tuned headers;
wenzelm [Sun, 13 Mar 2011 15:10:00 +0100] rev 41941
tuned headers;
Sun, 13 Mar 2011 14:51:38 +0100 allow spaces in executable names;
wenzelm [Sun, 13 Mar 2011 14:51:38 +0100] rev 41940
allow spaces in executable names; simplified generated bash scripts;
Sun, 13 Mar 2011 13:57:20 +0100 tuned;
wenzelm [Sun, 13 Mar 2011 13:57:20 +0100] rev 41939
tuned;
Sun, 13 Mar 2011 13:53:54 +0100 tuned headers;
wenzelm [Sun, 13 Mar 2011 13:53:54 +0100] rev 41938
tuned headers;
Fri, 11 Mar 2011 15:21:13 +0100 adapting example file to renaming of the quickcheck tester
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41937
adapting example file to renaming of the quickcheck tester
Fri, 11 Mar 2011 15:21:13 +0100 renaming tester from lazy_exhaustive to narrowing
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41936
renaming tester from lazy_exhaustive to narrowing
Fri, 11 Mar 2011 15:21:13 +0100 minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41935
minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common
Fri, 11 Mar 2011 15:21:13 +0100 renaming example file correctly
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41934
renaming example file correctly
Fri, 11 Mar 2011 15:21:13 +0100 adapting Main file generation for Quickcheck_Narrowing
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41933
adapting Main file generation for Quickcheck_Narrowing
Fri, 11 Mar 2011 15:21:13 +0100 adapting Quickcheck_Narrowing and example file to new names
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41932
adapting Quickcheck_Narrowing and example file to new names
Fri, 11 Mar 2011 15:21:13 +0100 renaming LSC_Examples theory to Quickcheck_Narrowing
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41931
renaming LSC_Examples theory to Quickcheck_Narrowing
Fri, 11 Mar 2011 15:21:13 +0100 renaming lazysmallcheck ML file to Quickcheck_Narrowing
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41930
renaming lazysmallcheck ML file to Quickcheck_Narrowing
Fri, 11 Mar 2011 15:21:13 +0100 renaming LSC to Quickcheck_Narrowing
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41929
renaming LSC to Quickcheck_Narrowing
Fri, 11 Mar 2011 15:21:13 +0100 adaptions in generators using the common functions
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41928
adaptions in generators using the common functions
Fri, 11 Mar 2011 15:21:13 +0100 adding file quickcheck_common to carry common functions of all quickcheck generators
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41927
adding file quickcheck_common to carry common functions of all quickcheck generators
Fri, 11 Mar 2011 15:21:13 +0100 adapting record package to renaming of quickcheck's structures
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41926
adapting record package to renaming of quickcheck's structures
Fri, 11 Mar 2011 15:21:13 +0100 moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41925
moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better
Fri, 11 Mar 2011 15:21:13 +0100 correcting dependencies in IsaMakefile
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41924
correcting dependencies in IsaMakefile
Fri, 11 Mar 2011 15:21:13 +0100 renaming signatures and structures; correcting header
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41923
renaming signatures and structures; correcting header
Fri, 11 Mar 2011 15:21:13 +0100 adapting Quickcheck theory after moving ML files
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41922
adapting Quickcheck theory after moving ML files
Fri, 11 Mar 2011 15:21:13 +0100 moving quickcheck_generators.ML to Quickcheck directory and renaming it random_generators.ML
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41921
moving quickcheck_generators.ML to Quickcheck directory and renaming it random_generators.ML
Fri, 11 Mar 2011 15:21:13 +0100 moving exhaustive_generators.ML to Quickcheck directory
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41920
moving exhaustive_generators.ML to Quickcheck directory
Fri, 11 Mar 2011 15:21:13 +0100 correcting dependencies after renaming
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41919
correcting dependencies after renaming
Fri, 11 Mar 2011 15:21:13 +0100 replacing naming of small by exhaustive
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41918
replacing naming of small by exhaustive
Fri, 11 Mar 2011 15:21:13 +0100 renaming smallvalue_generators.ML to exhaustive_generators.ML
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41917
renaming smallvalue_generators.ML to exhaustive_generators.ML
Fri, 11 Mar 2011 15:21:13 +0100 renaming constants in Quickcheck_Exhaustive theory
bulwahn [Fri, 11 Mar 2011 15:21:13 +0100] rev 41916
renaming constants in Quickcheck_Exhaustive theory
Fri, 11 Mar 2011 15:21:12 +0100 renaming Smallcheck to Quickcheck_Exhaustive
bulwahn [Fri, 11 Mar 2011 15:21:12 +0100] rev 41915
renaming Smallcheck to Quickcheck_Exhaustive
Fri, 11 Mar 2011 10:37:45 +0100 only testing theory LSC_Examples when GHC is installed on the machine
bulwahn [Fri, 11 Mar 2011 10:37:45 +0100] rev 41914
only testing theory LSC_Examples when GHC is installed on the machine
Fri, 11 Mar 2011 10:37:43 +0100 increasing timeout of example for counterexample generation
bulwahn [Fri, 11 Mar 2011 10:37:43 +0100] rev 41913
increasing timeout of example for counterexample generation
Fri, 11 Mar 2011 10:37:42 +0100 adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC
bulwahn [Fri, 11 Mar 2011 10:37:42 +0100] rev 41912
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 adding lazysmallcheck example theory to HOL-ex session
bulwahn [Fri, 11 Mar 2011 10:37:41 +0100] rev 41911
adding lazysmallcheck example theory to HOL-ex session
Fri, 11 Mar 2011 10:37:40 +0100 adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies
bulwahn [Fri, 11 Mar 2011 10:37:40 +0100] rev 41910
adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies
Fri, 11 Mar 2011 10:37:38 +0100 replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
bulwahn [Fri, 11 Mar 2011 10:37:38 +0100] rev 41909
replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype
Fri, 11 Mar 2011 10:37:37 +0100 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
bulwahn [Fri, 11 Mar 2011 10:37:37 +0100] rev 41908
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 adding an example theory for Lazysmallcheck prototype
bulwahn [Fri, 11 Mar 2011 10:37:37 +0100] rev 41907
adding an example theory for Lazysmallcheck prototype
Fri, 11 Mar 2011 10:37:36 +0100 adding Lazysmallcheck prototype to HOL-Library
bulwahn [Fri, 11 Mar 2011 10:37:36 +0100] rev 41906
adding Lazysmallcheck prototype to HOL-Library
Fri, 11 Mar 2011 10:37:35 +0100 adding files for prototype of lazysmallcheck
bulwahn [Fri, 11 Mar 2011 10:37:35 +0100] rev 41905
adding files for prototype of lazysmallcheck
Fri, 11 Mar 2011 08:58:29 +0100 removing debug message in quickcheck's postprocessor
bulwahn [Fri, 11 Mar 2011 08:58:29 +0100] rev 41904
removing debug message in quickcheck's postprocessor
Fri, 11 Mar 2011 08:13:00 +0100 fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
bulwahn [Fri, 11 Mar 2011 08:13:00 +0100] rev 41903
fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample
Fri, 11 Mar 2011 08:12:59 +0100 renaming dest_plain_fun to dest_fun_upds and adding handling of undefined for postprocessing of quickcheck
bulwahn [Fri, 11 Mar 2011 08:12:59 +0100] rev 41902
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 improving term postprocessing for counterexample presentation in quickcheck
bulwahn [Fri, 11 Mar 2011 08:12:58 +0100] rev 41901
improving term postprocessing for counterexample presentation in quickcheck
Fri, 11 Mar 2011 08:12:55 +0100 tuned
bulwahn [Fri, 11 Mar 2011 08:12:55 +0100] rev 41900
tuned
Wed, 09 Mar 2011 21:40:38 +0100 finished and tested Z3 proof reconstruction for injective functions;
boehmes [Wed, 09 Mar 2011 21:40:38 +0100] rev 41899
finished and tested Z3 proof reconstruction for injective functions; only treat variables as atomic, and especially abstract constants (Isabelle's interpretation of these constants is most likely not known to Z3 and thus irrelevant for the proof)
Wed, 09 Mar 2011 10:28:01 +0100 improved formula for specialization, to prevent needless specializations -- and removed dead code
blanchet [Wed, 09 Mar 2011 10:28:01 +0100] rev 41898
improved formula for specialization, to prevent needless specializations -- and removed dead code
Wed, 09 Mar 2011 10:25:29 +0100 perform no arity check in debug mode so that we get to see the Kodkod problem
blanchet [Wed, 09 Mar 2011 10:25:29 +0100] rev 41897
perform no arity check in debug mode so that we get to see the Kodkod problem
Fri, 04 Mar 2011 17:39:30 +0100 spark_end now joins proofs of VCs before writing *.prv file.
berghofe [Fri, 04 Mar 2011 17:39:30 +0100] rev 41896
spark_end now joins proofs of VCs before writing *.prv file.
Fri, 04 Mar 2011 11:43:20 +0100 clarified
krauss [Fri, 04 Mar 2011 11:43:20 +0100] rev 41895
clarified
Fri, 04 Mar 2011 11:52:54 +0100 produce helpful mira summary for more errors
krauss [Fri, 04 Mar 2011 11:52:54 +0100] rev 41894
produce helpful mira summary for more errors
Fri, 04 Mar 2011 00:09:47 +0100 eliminated prems;
wenzelm [Fri, 04 Mar 2011 00:09:47 +0100] rev 41893
eliminated prems;
Thu, 03 Mar 2011 22:06:15 +0100 eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;
wenzelm [Thu, 03 Mar 2011 22:06:15 +0100] rev 41892
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 tuned proofs -- eliminated prems;
wenzelm [Thu, 03 Mar 2011 21:43:06 +0100] rev 41891
tuned proofs -- eliminated prems;
Thu, 03 Mar 2011 18:43:15 +0100 merged
wenzelm [Thu, 03 Mar 2011 18:43:15 +0100] rev 41890
merged
Thu, 03 Mar 2011 14:38:31 +0100 merged
blanchet [Thu, 03 Mar 2011 14:38:31 +0100] rev 41889
merged
Thu, 03 Mar 2011 14:25:15 +0100 don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
blanchet [Thu, 03 Mar 2011 14:25:15 +0100] rev 41888
don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip