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