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

redo more Metis/Sledgehammer example

fixed definition of "bad frees" so that it actually works

don't remove last line of proof

handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction

make SML/NJ happy, take 2

use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)

expand combinators in Isar proofs constructed by Sledgehammer;
this requires shuffling around a couple of functions previously defined in Refute

more neg_clausify proofs that get replaced by direct proofs

redo some of the metis proofs

back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs