ep_pair and deflation lemmas for powerdomain map functions

remove spurious parameter to "merge"

merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)

fixed soundness bug in Nitpick related to sets of sets; (detected thanks to the TPTP)

added possibility to register datatypes as codatatypes in Nitpick; this is useful if the datatype is used only as a means to define the codatatype

added datatype constructor cache in Nitpick (to speed up the scope enumeration) and never test more than 4096 scopes

don't promise too much in the Nitpick manual

merged

added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package; this ensures that Nitpick can find the definition and determine whether its inductive or coinductive

merged

try very hard to remove temporary files generated by Nitpick in case of interruption

eliminate two FIXMEs in Nitpick's monotonicity check code

rename "NitpickMono" to "Nitpick_Mono" in example

merged

minor cleanup in Nitpick

make "auto" SAT solver less verbose

make "sizechange_tac" slightly less verbose

don't run Nitpick at all if Kodkodi is not installed (as indicated by the $KODKODI variable)

readded Predicate_Compile to Main

merged

fixed error in Nitpick's display of uncurried constants, which resulted in an exception

fixed minor problems with Nitpick's documentation

merged

merged my Auto Nitpick change with Lukas's Predicate Compiler changes

introduced Auto Nitpick in addition to Auto Quickcheck; this required generalizing the theorem hook used by Quickcheck, following a suggestion by Florian

use "get_goal" rather than "flat_goal" in Auto Quickcheck, since we don't need the extra facts for counterexample generation

fix typo in Nitpick manual

optimized Nitpick's encoding and rendering of datatypes whose constructors don't appear in the problem

clean Nitpick's wellfoundedness cache once in a while, to avoid potential memory leak

renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary

eliminated some old uses of cumulative prems (!) in proof methods;

eliminated some unused/obsolete Args.bang_facts;

modernized structure Theory_Target;

removed unused Quickcheck_RecFun_Simps;

define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;

bang_facts: legacy feature;

tuned proofs;

removed obsolete name_of -- cf. decode;

desymbolize: use Symbol.decode directly; recovered coding conventions of this file;

try SAT_Examples last, to minimize impact of global side-effects;

home-grown pretty printer for term -- Poly/ML 5.3.0 does not observe infix status of constructors (notably $);

Inserted missing theory dependency

merged

Merged.

Removed obsolete code.

updated to official Poly/ML 5.3.0;

switched some isatest sessions to official Poly/ML 5.3.0;

setup for official Poly/ML 5.3.0, which is now the default;

locale_const/target_notation: uniform use of Term.aconv_untyped; target_notation: pass on transformed term formally; removed obsolete Type.similar_types;

eliminated hard tabulators;

fixed some inappropriate names

merged

New theory Probability/Borel.thy, and some associated lemmas

merged

tuned error messages; tuned code

follow standard theory merge behaviour: do not change already selected solver