isabelle: Graph

made sure to filter type args also for "uncurried alias" equations
2012-02-04, by blanchet
made option available to users (mostly for experiments)
2012-02-04, by blanchet
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4 (also cf. 0fd9ab902b5a)
2012-02-04, by bulwahn
optimization: slice caching in case two consecutive slices are nearly identical
2012-02-03, by blanchet
extended SPASS/DFG output with ranks
2012-02-03, by blanchet
try to pass fewer options to Metis
2012-02-03, by blanchet
Quotient FSet: Add compositional respectfulness and preservation for map and lift map_concat
2012-02-03, by Cezary Kaliszyk
improve SPASS scripts
2012-02-02, by blanchet
change 9ce354a77908 wasn't quite right -- here's an improvement
2012-02-02, by blanchet
better SPASS setup
2012-02-02, by blanchet
don't introduce new symbols in helpers -- makes problems unprovable
2012-02-02, by blanchet
only constants can be aliased
2012-02-02, by blanchet
include new SPASS by default if available
2012-02-02, by blanchet
adding an example for finite and cofinite sets
2012-02-02, by bulwahn
adding a minimally refined equality on sets for code generation
2012-02-02, by bulwahn
adding an example for a datatype refinement which would allow rtrancl to be executable on an infinite type
2012-02-02, by bulwahn
improving code equations for multisets that violated the distinct AList abstraction
2012-02-01, by bulwahn
tuning
2012-02-02, by blanchet
implemented partial application aliases (for SPASS mainly)
2012-02-02, by blanchet
really fixed syntax bug in DFG output (cf. ef62c2fafa9e)
2012-02-01, by blanchet
don't stumble on SPASS debug output
2012-02-01, by blanchet
tuning
2012-02-01, by blanchet
proper statuses for "fact_from_ref"
2012-02-01, by blanchet
tuned
2012-01-31, by nipkow
renamed Sledgehammer option
2012-01-31, by blanchet
third attempt at lambda lifting that works for both Sledgehammer and Metis (cf. dce6c3a460a9)
2012-01-31, by blanchet
improve SPASS setup
2012-01-31, by blanchet
adding code equation for setsum
2012-01-31, by bulwahn
avoid name clash, really
2012-01-31, by blanchet
fixed syntax bug in DFG output
2012-01-31, by blanchet
new SPASS setup
2012-01-31, by blanchet
distinguish between ":lr" and ":lt" (terminating) in DFG format
2012-01-31, by blanchet
nicer keyword class avoidance scheme
2012-01-31, by blanchet
new try at lambda-lifting that works correctly for both Metis and Sledgehammer (cf. d724066ff3d0)
2012-01-31, by blanchet
mutabelle must handle the case where quickcheck returns multiple results
2012-01-31, by bulwahn
reverted e2b1a86d59fc -- broke Metis's lambda-lifting
2012-01-31, by blanchet
merged
2012-01-31, by nipkow
NEWS
2012-01-31, by nipkow
added "'a rel"
2012-01-30, by nipkow
fix debilitating bug with lambda lifting in conjectures with outer existential quantifiers
2012-01-30, by blanchet
new SPASS setup
2012-01-30, by blanchet
example tuning
2012-01-30, by blanchet
implemented new lambda translations scheme
2012-01-30, by blanchet
avoid unsupported case in Metis
2012-01-30, by blanchet
docs and news
2012-01-30, by blanchet
rename lambda translation schemes
2012-01-30, by blanchet
example tuning
2012-01-30, by blanchet
NEWS
2012-01-30, by bulwahn
renaming all lemmas with name rel_pow to relpow
2012-01-30, by bulwahn
adding code equations for max_extp and mlex
2012-01-30, by bulwahn
adding code generation for relpow by copying the ideas for code generation of funpow
2012-01-30, by bulwahn
adding code equation for rtranclp in Enum
2012-01-30, by bulwahn
adding code equation for max_ext
2012-01-30, by bulwahn
adding code equation for tranclp
2012-01-30, by bulwahn
adding code_unfold to make measure executable
2012-01-30, by bulwahn
removed accidental dependance of abstract interpreter on gamma
2012-01-29, by nipkow
merged
2012-01-29, by nipkow
tuned
2012-01-29, by nipkow
an executable version of accessible part (only for finite types yet)
2012-01-28, by bulwahn
adding yet another induction rule on natural numbers
2012-01-28, by bulwahn
moving declarations back to the section they seem to belong to (cf. afffe1f72143)
2012-01-28, by bulwahn
reverting 46c2c96f5d92 as it only provides mostly non-terminating executions for generated code
2012-01-28, by bulwahn
adding some more examples for quickcheck; replaced FIXME comments
2012-01-27, by bulwahn
new code equation for ntrancl that allows computation of the transitive closure of sets on infinite types as well
2012-01-27, by bulwahn
removed duplicate definitions that made locale inconsistent
2012-01-27, by nipkow
added parity analysis
2012-01-27, by nipkow
corrected expectation; added an example for quickcheck
2012-01-27, by bulwahn
adding some basic handling that unfolds a conjecture in a locale before testing it with quickcheck
2012-01-27, by bulwahn
made SML/NJ happy
2012-01-27, by blanchet
even more lr tags for SPASS -- anything that is considered an "equational rule spec" is relevant
2012-01-26, by blanchet
separate orthogonal components
2012-01-26, by blanchet
generate left-to-right rewrite tag for combinator helpers for SPASS 3.8
2012-01-26, by blanchet
better handling of individual type for DFG format (SPASS)
2012-01-26, by blanchet
adding quickcheck example with THE
2012-01-26, by bulwahn
evaluation of THE with a non-singleton set raises a Match exception during the evaluation to yield a potential counterexample in quickcheck.
2012-01-26, by bulwahn
using fully qualified module names in Haskell source, which seems to be required by GHC 7.0.4
2012-01-26, by bulwahn
tuned
2012-01-26, by nipkow
adding very basic code generation to Wellfounded theory
2012-01-25, by bulwahn
removing dead code from Mutabelle; tuned
2012-01-25, by bulwahn
generalizing check if size matters because it is different for random and exhaustive testing
2012-01-25, by bulwahn
merged
2012-01-25, by bulwahn
adding code equation for Collect on finite types
2012-01-25, by bulwahn
Use lookup_size rather than Datatype.get_info in is_poly to avoid
2012-01-24, by berghofe
adding some rules to quickcheck's preprocessing
2012-01-24, by bulwahn
some more constants on mutabelle's blacklist
2012-01-24, by bulwahn
implemented "tptp_refute" tool
2012-01-23, by blanchet
added problem importer
2012-01-23, by blanchet
imported patch ATP_Problem_Import.thy
2012-01-23, by blanchet
imported patch atp_problem_import.ML
2012-01-23, by blanchet
renamed theory exporter
2012-01-23, by blanchet
renamed two files to make room for a new file
2012-01-23, by blanchet
rebranded Nitrox, for more uniformity
2012-01-23, by blanchet
moved "nitrox" to TPTP
2012-01-23, by blanchet
generalize type of List.listrel
2012-01-23, by huffman
support for Ex1 in quickcheck-narrowing
2012-01-23, by bulwahn
adding another internal constant to mutabelle's blacklust
2012-01-23, by bulwahn