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

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

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

stengthened tactic to cope with abort cases

tuned names

strengthened tactic w.r.t. "let"

more prominent MaSh errors

compile -- fix typo introduced in 07a8145aaeba

pass the right theorems to tactic

prove user-supplied equations for ctr and code reductions, preserving "let"s, "case"s etc.;
generate code-style theorems (currently commented out since this still fails for many cases);
filter tautologies (False ==> ...) out of generated theorems;

repaired confusion between the stated and effective fact filter -- the mismatch could result in "Match" exceptions

simplify fudge factor code

cleanup SMT-related config options