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

generalized proof by abstraction, abstract propositional nnf goals (lets best_tac succeed on very large terms)

made theory merge deterministic wrt. the selected solver

merged

merged

Repaired handling of comprehensions in "values" command.

updated functor Theory_Data, Proof_Data, Generic_Data;

modernized structure Reorient_Proc; explicit merge of constituent functions, avoids exponential blowup when traversing the import graph; adapted Theory_Data; tuned;

adapted Theory_Data; tuned;

adapted Theory_Data; handle Symtab.DUP during actual merge;

tuned;

adapted Generic_Data, Proof_Data; tuned;

adapted Generic_Data; proper merge of fst/fst and snd/snd;

modernized/simplified functor Theory_Data, Proof_Data, Generic_Data: eliminated Pretty.pp, discontinued mutable data;

added "declaration (pervasive)";

print_theorems: suppress concealed (global) facts, unless "!" option is given;

updated generated file;

modernized structure Random_Word;