2012-02-05 bulwahn 2012-02-05 another try to improve code generation of set equality (cf. da32cf32c0c7)
2012-02-05 bulwahn 2012-02-05 beautifying definitions of check_all and adding instance for finite_4
2012-02-05 Cezary Kaliszyk 2012-02-05 Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
2012-02-04 blanchet 2012-02-04 added option to Mirabelle/Sledgehammer
2012-02-04 blanchet 2012-02-04 improved hashing w.r.t. Mirabelle, to help debugging
2012-02-04 blanchet 2012-02-04 tuned SPASS DFG output
2012-02-04 blanchet 2012-02-04 the new SPASS gives accurate fact information, so no need for old hack anymore
2012-02-04 blanchet 2012-02-04 fixed docs
2012-02-04 blanchet 2012-02-04 made sure to filter type args also for "uncurried alias" equations
2012-02-04 blanchet 2012-02-04 made option available to users (mostly for experiments)
2012-02-04 bulwahn 2012-02-04 using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)
2012-02-03 blanchet 2012-02-03 optimization: slice caching in case two consecutive slices are nearly identical
2012-02-03 blanchet 2012-02-03 extended SPASS/DFG output with ranks
2012-02-03 blanchet 2012-02-03 try to pass fewer options to Metis
2012-02-03 Cezary Kaliszyk 2012-02-03 Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
2012-02-02 blanchet 2012-02-02 improve SPASS scripts
2012-02-02 blanchet 2012-02-02 change 9ce354a77908 wasn't quite right -- here's an improvement
2012-02-02 blanchet 2012-02-02 better SPASS setup
2012-02-02 blanchet 2012-02-02 don't introduce new symbols in helpers -- makes problems unprovable
2012-02-02 blanchet 2012-02-02 only constants can be aliased
2012-02-02 blanchet 2012-02-02 include new SPASS by default if available
2012-02-02 bulwahn 2012-02-02 adding an example for finite and cofinite sets
2012-02-02 bulwahn 2012-02-02 adding a minimally refined equality on sets for code generation
2012-02-02 bulwahn 2012-02-02 adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
2012-02-01 bulwahn 2012-02-01 improving code equations for multisets that violated the distinct AList abstraction
2012-02-02 blanchet 2012-02-02 tuning
2012-02-02 blanchet 2012-02-02 implemented partial application aliases (for SPASS mainly)
2012-02-01 blanchet 2012-02-01 really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
2012-02-01 blanchet 2012-02-01 don't stumble on SPASS debug output
2012-02-01 blanchet 2012-02-01 tuning
2012-02-01 blanchet 2012-02-01 proper statuses for "fact_from_ref"
2012-01-31 nipkow 2012-01-31 tuned
2012-01-31 blanchet 2012-01-31 renamed Sledgehammer option
2012-01-31 blanchet 2012-01-31 third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
2012-01-31 blanchet 2012-01-31 improve SPASS setup
2012-01-31 bulwahn 2012-01-31 adding code equation for setsum
2012-01-31 blanchet 2012-01-31 avoid name clash, really
2012-01-31 blanchet 2012-01-31 fixed syntax bug in DFG output
2012-01-31 blanchet 2012-01-31 new SPASS setup
2012-01-31 blanchet 2012-01-31 distinguish between ":lr" and ":lt" (terminating) in DFG format
2012-01-31 blanchet 2012-01-31 nicer keyword class avoidance scheme
2012-01-31 blanchet 2012-01-31 new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)
2012-01-31 bulwahn 2012-01-31 mutabelle must handle the case where quickcheck returns multiple results
2012-01-31 blanchet 2012-01-31 reverted e2b1a86d59fc -- broke Metis's lambda-lifting
2012-01-31 nipkow 2012-01-31 merged
2012-01-31 nipkow 2012-01-31 NEWS
2012-01-30 nipkow 2012-01-30 added "'a rel"
2012-01-30 blanchet 2012-01-30 fix debilitating bug with lambda lifting in conjectures with outer existential quantifiers
2012-01-30 blanchet 2012-01-30 new SPASS setup
2012-01-30 blanchet 2012-01-30 example tuning
2012-01-30 blanchet 2012-01-30 implemented new lambda translations scheme
2012-01-30 blanchet 2012-01-30 avoid unsupported case in Metis
2012-01-30 blanchet 2012-01-30 docs and news
2012-01-30 blanchet 2012-01-30 rename lambda translation schemes
2012-01-30 blanchet 2012-01-30 example tuning
2012-01-30 bulwahn 2012-01-30 NEWS
2012-01-30 bulwahn 2012-01-30 renaming all lemmas with name rel_pow to relpow
2012-01-30 bulwahn 2012-01-30 adding code equations for max_extp and mlex
2012-01-30 bulwahn 2012-01-30 adding code generation for relpow by copying the ideas for code generation of funpow
2012-01-30 bulwahn 2012-01-30 adding code equation for rtranclp in Enum