isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -30000 -10000 -3000 -1000 -300 -100 -15 +15 +100 +300 +1000 +3000 +10000 +30000 tip

generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
2010-12-15, by blanchet
make sure first-order occurrences of "False" and "True" are handled correctly -- this broke when adding proper support for higher-order occurrences
2010-12-15, by blanchet
consider "finite" overloaded in "precise_overloaded_args" mode
2010-12-15, by blanchet
added timeout max for remote server invocation
2010-12-15, by blanchet
fix translation of higher-order equality ("fequal") if "precise_overloaded_args" is "true"
2010-12-15, by blanchet
fix Vampire parsing problem
2010-12-15, by blanchet
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
2010-12-15, by blanchet
example tuning
2010-12-15, by blanchet
remove at most one double negation -- any other double negations are part of some higher-order reasoning and should be left alone, cf. "HO_Reas.thy"
2010-12-15, by blanchet
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed
2010-12-15, by blanchet
added example to exercise higher-order reasoning with Sledgehammer and Metis
2010-12-15, by blanchet
added Sledgehammer support for higher-order propositional reasoning
2010-12-15, by blanchet
add Metis support for higher-order propositional reasoning
2010-12-15, by blanchet
implemented partially-typed "tags" type encoding
2010-12-15, by blanchet
implemented "no_types" encoding, which is too unsound to be useful but can come in handy for evaluations
2010-12-15, by blanchet

less more | (0) -30000 -10000 -3000 -1000 -300 -100 -15 +15 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle