minor DFG fix

new SPASS slices

improved KBO weights -- beware of explicit applications

added possibility of generating KBO weights to DFG problems

Generalize the compositional preservation theorems

use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")

removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly

beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms

fixed arity error

tuning

renamed type encoding

adding some forbidden constant names for mutabelle

mutabelle ignores theorems with internal constants

tuned

merged

simplified code generation

remove option that's on by default

no need for a script/mega-hack with the new SPASS

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