new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well

removed duplicate definitions that made locale inconsistent

added parity analysis

corrected expectation; added an example for quickcheck

adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck

made SML/NJ happy

even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant

separate orthogonal components

generate left-to-right rewrite tag for combinator helpers for SPASS 3.8

better handling of individual type for DFG format (SPASS)

adding quickcheck example with THE

evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.

using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4

tuned

adding very basic code generation to Wellfounded theory

removing dead code from Mutabelle; tuned

generalizing check if size matters because it is different for random and exhaustive testing

merged

adding code equation for Collect on finite types

Use lookup_size rather than Datatype.get_info in is_poly to avoid incorrect results for datatypes on which no size function is defined

adding some rules to quickcheck's preprocessing

some more constants on mutabelle's blacklist

implemented "tptp_refute" tool

added problem importer

imported patch ATP_Problem_Import.thy

imported patch atp_problem_import.ML

renamed theory exporter

renamed two files to make room for a new file