spurious proof failure

merged

merged

dropped unused binding

dedicated conversions to and from Int

printing of cases

tuned for products vs. tupled functions

added Scala setup

allow individual printing of numerals during code serialization

reorder Quickcheck and Nitpick, so that Quickcheck gets loaded first and Auto-Quickcheck runs first (since it takes less time)

adjusted to changes in code equation administration

explicit abstract type of code certificates

corrected error messages; tuned

function transformer preprocessor applies to both code generators

merged

code certificates as integral part of code generation

import of antiquote_setup not necessary

merged

being more accurate wrt. list syntax

deactivate pretty code test for Scala -- no proper setup yet

some syntax setup for Scala

added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;

merged

Parsing errors during proof reconstruction now give rise to an intelligible error message.

rebuilt from fresh copy of Bitstream Vera, for improved quality of regular text glyphs; misc cleanup of mathematical glyphs, with bold version synthesized by fontforge;

tuned initial properties/perspective;

provide JEDIT_SETTINGS via settings; provide default perspective; tuned default properties;

updated version and dependencies;