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