more conventional Mutabelle settings -- similar to Mirabelle;

more basic use of Path.position/File.read;

prefer qualified ISABELLE_NEOS_SERVER;

proper File.shell_path;

more conventional variable name;

Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;

fixed document;

isatest: test more external code;

tuned headers;

allow spaces in executable names; simplified generated bash scripts;

tuned;

tuned headers;

adapting example file to renaming of the quickcheck tester

renaming tester from lazy_exhaustive to narrowing

minor corrections for renaming; moved postprocessing of terms to Quickcheck_Common

renaming example file correctly

adapting Main file generation for Quickcheck_Narrowing

adapting Quickcheck_Narrowing and example file to new names

renaming LSC_Examples theory to Quickcheck_Narrowing

renaming lazysmallcheck ML file to Quickcheck_Narrowing

renaming LSC to Quickcheck_Narrowing

adaptions in generators using the common functions

adding file quickcheck_common to carry common functions of all quickcheck generators

adapting record package to renaming of quickcheck's structures

moving and renaming lazysmallcheck to narrowing which reflects the characteristical behaviour better

correcting dependencies in IsaMakefile

renaming signatures and structures; correcting header

adapting Quickcheck theory after moving ML files

moving quickcheck_generators.ML to Quickcheck directory and renaming it random_generators.ML

moving exhaustive_generators.ML to Quickcheck directory

correcting dependencies after renaming

replacing naming of small by exhaustive

renaming smallvalue_generators.ML to exhaustive_generators.ML

renaming constants in Quickcheck_Exhaustive theory

renaming Smallcheck to Quickcheck_Exhaustive

only testing theory LSC_Examples when GHC is installed on the machine

increasing timeout of example for counterexample generation

adding termination proofs to series functions in LSC; commenting out momentarily unused term refinement functions in LSC

adding lazysmallcheck example theory to HOL-ex session

adding serial instance of finite_4 in lazysmallcheck; changing code equations for implies

replacing strings in generated Code resolves the changing names of Typerep in lazysmallcheck prototype

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

adding an example theory for Lazysmallcheck prototype

adding Lazysmallcheck prototype to HOL-Library

adding files for prototype of lazysmallcheck

removing debug message in quickcheck's postprocessor

fixing postprocessing; adding a configuration to enable and disable pretty presentation of quickcheck's counterexample

renaming dest_plain_fun to dest_fun_upds and adding handling of undefined for postprocessing of quickcheck

improving term postprocessing for counterexample presentation in quickcheck

tuned

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)

improved formula for specialization, to prevent needless specializations -- and removed dead code

perform no arity check in debug mode so that we get to see the Kodkod problem

spark_end now joins proofs of VCs before writing *.prv file.

clarified

produce helpful mira summary for more errors

eliminated prems;

eliminated UNITY_Examples.thy which takes quite long to merge and does not parallelize so well -- essentially reverting 3dec57ec3473;

tuned proofs -- eliminated prems;

merged