summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

merged

add an Isar proof found with Sledgehammer that involves a Skolem constant (internally)

reintroduced short names for HOL->FOL constants; other parts of the code rely on these

save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code

unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)

redo Sledgehammer proofs (and get rid of "neg_clausify")

removed "sorts" option, continued

remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
what we need is smarter type annotations for variables _and_ constants

insert a nice proof found by Vampire, which demonstrates the use of "let" in Isar proofs

support Vampire definitions of constants as "let" constructs in Isar proofs