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

merged

don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on

simplified Thy_Info.check_file -- discontinued load path;

discontinued legacy load path;

re-interpret ProofGeneralPgip.changecwd as Thy_Load.set_master_path, presuming that this is close to the intended semantics;

modernized imports;

observe standard header format;

removed spurious 'unused_thms' (cf. 1a65b780bd56);

isatest cygwin-poly-e: new memory management of polyml-svn could be more stable;

merged

merged

- Made sure that sort_defs is aware of constants introduced by add_type_def - add_def now compares Isabelle types rather than SPARK types to ensure that type abbreviations are taken into account

mention new Nitpick options

simplify "need" option's syntax

renamed "preconstr" option "need"

finally remove upper_bound_finite_set

separate settings for afp test

added missing spaces in output

lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on

unfold definitions in "preconstrs" option

robust handling of types occurring in "eval" and "preconstr" options but not in the goal

make "preconstr" option more robust -- shouldn't throw exceptions

merged

merged

declare ext [intro]: Extensionality now available by default

merged

removed dependency on Dense_Linear_Order

adding function Quickcheck.test_terms to provide checking a batch of terms

adding a function to compile a batch of terms for quickcheck with one code generation invocation

improved "is_special_eligible_arg" further, by approximating the cardinality of the argument (as is done quite successfully elsewhere)

made "fixed_is_special_eligible_arg" smarter w.r.t. pairs, and fixed previous unintended behavior because "andalso" ties more tightly than "orelse"

if "total_consts" is set, report cex's as quasi-genuine

document new "total_consts" option

added "total_consts" option

added a few lemmas by Andreas Lochbihler

Corrected HOLCF/FOCUS dependency

Added material by David Trachtenherz

corrected HOLCF dependency on Nat_Infinity

got rid of lemma upper_bound_finite_set

merged

Some cleaning up

updated generated files

fixed manual (rule no longer exists)

removed support for tail-recursion from function package (now implemented by partial_function)

reactivate time measurement (partly reverting c27b0b37041a); export pretty_theorem, to display both internal or external facts

generalize find_theorems filters to work on raw propositions, too

merged