isabelle: Graph

normalized aliases;
2012-02-14, by wenzelm
elininated unused INTLEAVE;
2012-02-14, by wenzelm
eliminated unused rewrite_goal_rule;
2012-02-14, by wenzelm
eliminated unused subgoals_tac;
2012-02-14, by wenzelm
eliminated obsolete aliases;
2012-02-14, by wenzelm
eliminated obsolete aliases;
2012-02-14, by wenzelm
tuned;
2012-02-14, by wenzelm
merged, resolving trivial conflicts;
2012-02-14, by wenzelm
merged;
2012-02-14, by wenzelm
new SPASS options
2012-02-11, by blanchet
making num_mutations a configuration that can be changed with the mutabelle bash command
2012-02-11, by bulwahn
making max_mutants an option that can be changed in the Mutabelle-script
2012-02-11, by bulwahn
increase timeout to 30 seconds; changing mutabelle script
2012-02-11, by bulwahn
parse clauses generated from several formulas
2012-02-10, by blanchet
be more gentle when generating KBO weights
2012-02-10, by blanchet
update SPASS slices
2012-02-10, by blanchet
more specification of the quotient package in IsarRef
2012-02-10, by Cezary Kaliszyk
specification of the quotient package
2012-02-10, by Cezary Kaliszyk
tune KBO weight code
2012-02-09, by blanchet
minor DFG fix
2012-02-09, by blanchet
new SPASS slices
2012-02-09, by blanchet
improved KBO weights -- beware of explicit applications
2012-02-09, by blanchet
added possibility of generating KBO weights to DFG problems
2012-02-09, by blanchet
Generalize the compositional preservation theorems
2012-02-09, by Cezary Kaliszyk
use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
2012-02-08, by blanchet
removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
2012-02-08, by blanchet
beware of "Bit0" and "Bit1" -- these shouldn't be blidly unfolded by SPASS, lest we get gigantic terms
2012-02-08, by blanchet
fixed arity error
2012-02-06, by blanchet
tuning
2012-02-06, by blanchet
renamed type encoding
2012-02-06, by blanchet
adding some forbidden constant names for mutabelle
2012-02-05, by bulwahn
mutabelle ignores theorems with internal constants
2012-02-05, by bulwahn
tuned
2012-02-05, by nipkow
merged
2012-02-05, by nipkow
simplified code generation
2012-02-05, by nipkow
remove option that's on by default
2012-02-05, by blanchet
no need for a script/mega-hack with the new SPASS
2012-02-05, by blanchet
cleaned up new SPASS parsing
2012-02-05, by blanchet
tuning
2012-02-05, by blanchet
merged
2012-02-05, by bulwahn
adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
2012-02-05, by bulwahn
tuning to remove ML warnings
2012-02-05, by bulwahn
removed double filtering of type args
2012-02-05, by blanchet
adding a quickcheck example about functions and sets
2012-02-05, by bulwahn
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)
2012-02-05, by bulwahn
adding a remark about lemma which is too special and should be removed
2012-02-05, by bulwahn
another try to improve code generation of set equality (cf. da32cf32c0c7)
2012-02-05, by bulwahn
beautifying definitions of check_all and adding instance for finite_4
2012-02-05, by bulwahn
Make automatic derivation of raw/quotient types more greedy to allow descending and quot_lifted for compound quotients.
2012-02-05, by Cezary Kaliszyk
added option to Mirabelle/Sledgehammer
2012-02-04, by blanchet
improved hashing w.r.t. Mirabelle, to help debugging
2012-02-04, by blanchet
tuned SPASS DFG output
2012-02-04, by blanchet
the new SPASS gives accurate fact information, so no need for old hack anymore
2012-02-04, by blanchet
fixed docs
2012-02-04, by blanchet
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