clarifying the Predicate_Compile_Core signature

adding signature to Predicate_Compile_Aux; tuning Predicate_Compile_Aux structure

putting compilation setup of predicate compiler in a separate file

simplify fold_graph proofs

NEWS

removed dead code; fixed typo

switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)

merged

adding skip_proof in the examples because proof procedure cannot handle alternative compilations yet

tuned

generalized alternative functions to alternative compilation to handle arithmetic functions better

correcting alternative functions with tuples

no specialisation for patterns with only tuples in the predicate compiler

adding registration of functions in the function flattening

added book-keeping, registration and compilation with alternative functions for predicates in the predicate compiler

adding specialisation examples of the predicate compiler

adding specialisation of predicates to the predicate compiler

returning an more understandable user error message in the values command

adding Lazy_Sequences with explicit depth-bound

removing fishing for split thm in the predicate compiler

prefer recursive calls before others in the mode inference

added statistics to values command for random generation

adopting Predicate_Compile_Quickcheck

made quickcheck generic with respect to which compilation; added random compilation to quickcheck

removed yieldn in Lazy_Sequence and put in the ML structure; corrects behaviour of values command

adding a hook for experiments in the predicate compilation process

removing simple equalities in introduction rules in the predicate compiler

adopting Predicate_Compile

adding values command for new monad; added new random monad compilation to predicate_compile_quickcheck

generalizing the compilation process of the predicate compiler