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

adopting proposed_modes; adding a new dimension of complexity for nicer error messages; tuned

check if equations are present for all functions to avoid low-level exception later

anti_sym -> antisym

optionally trace theorems used in proof reconstruction

added arithmetic example using div and mod

bump up Nitpick's axiom/definition unfolding limits, because some real-world problems (e.g. from Boogie) ran into the previous limits;
the limits are there to prevent infinite recursion; they can be set arbitrarily high without much harm

merged

comment out debugging code in Nitpick

fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"

made "NitpickHOL.normalized_rhs_of" more robust in the face of locale definitions