Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest of the error message ("The exception above was raised for...") will appear. And print_exn calls print_sign_exn_unit so that it can re-raise the SAME exception.

Updated the "version" variable (which was never done for Isabelle-94 revisions 1 and 2!)

Redefined functions to suppress redundant leading 0s and 1s

new in mixfix annotations: "' " (quote space) separates delimiters without adding extra white space for printing;

Added the exception handler handle _ => exit 1. This will catch all errors and force an exit with error code, causing Make to fail.

intro_tacsf now includes subsetI as an introduction rule. It is needed for rules like list_into_univ

Updated comment about list_subset_univ and list_into_univ.

exit: new, for use in Makefiles

Redefined arithmetic to suppress redundant leading 0s and 1s renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.

Added integer numerals (mostly due to Markus Wenzel) renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.