cleaned up new SPASS parsing

tuning

merged

adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists

tuning to remove ML warnings

removed double filtering of type args

adding a quickcheck example about functions and sets

removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)

adding a remark about lemma which is too special and should be removed

another try to improve code generation of set equality (cf. da32cf32c0c7)

beautifying definitions of check_all and adding instance for finite_4

Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.

added option to Mirabelle/Sledgehammer

improved hashing w.r.t. Mirabelle, to help debugging

tuned SPASS DFG output

the new SPASS gives accurate fact information, so no need for old hack anymore

fixed docs

made sure to filter type args also for "uncurried alias" equations

made option available to users (mostly for experiments)

using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)

optimization: slice caching in case two consecutive slices are nearly identical

extended SPASS/DFG output with ranks

try to pass fewer options to Metis

Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat

improve SPASS scripts

change 9ce354a77908 wasn't quite right -- here's an improvement

better SPASS setup

don't introduce new symbols in helpers -- makes problems unprovable

only constants can be aliased

include new SPASS by default if available

adding an example for finite and cofinite sets

adding a minimally refined equality on sets for code generation

adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type

improving code equations for multisets that violated the distinct AList abstraction

tuning

implemented partial application aliases (for SPASS mainly)

really fixed syntax bug in DFG output (cf. ef62c2fafa9e)

don't stumble on SPASS debug output

tuning

proper statuses for "fact_from_ref"

tuned

renamed Sledgehammer option

third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)

improve SPASS setup

adding code equation for setsum

avoid name clash, really

fixed syntax bug in DFG output

new SPASS setup

distinguish between ":lr" and ":lt" (terminating) in DFG format

nicer keyword class avoidance scheme

new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)

mutabelle must handle the case where quickcheck returns multiple results

reverted e2b1a86d59fc -- broke Metis's lambda-lifting

merged

NEWS

added "'a rel"

fix debilitating bug with lambda lifting in conjectures with outer existential quantifiers

new SPASS setup

example tuning

implemented new lambda translations scheme

avoid unsupported case in Metis

docs and news

rename lambda translation schemes

example tuning

NEWS

renaming all lemmas with name rel_pow to relpow

adding code equations for max_extp and mlex

adding code generation for relpow by copying the ideas for code generation of funpow

adding code equation for rtranclp in Enum

adding code equation for max_ext

adding code equation for tranclp

adding code_unfold to make measure executable

removed accidental dependance of abstract interpreter on gamma

merged

tuned

an executable version of accessible part (only for finite types yet)

adding yet another induction rule on natural numbers

moving declarations back to the section they seem to belong to (cf. afffe1f72143)

reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code

adding some more examples for quickcheck; replaced FIXME comments

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

rebranded Nitrox, for more uniformity

moved "nitrox" to TPTP

generalize type of List.listrel

support for Ex1 in quickcheck-narrowing