Mon, 27 Feb 1995 17:47:44 +0100 Added the exception handler
lcp [Mon, 27 Feb 1995 17:47:44 +0100] rev 910
Added the exception handler handle _ => exit 1. This will catch all errors and force an exit with error code, causing Make to fail.
Mon, 27 Feb 1995 17:44:43 +0100 intro_tacsf now includes subsetI as an introduction rule. It is
lcp [Mon, 27 Feb 1995 17:44:43 +0100] rev 909
intro_tacsf now includes subsetI as an introduction rule. It is needed for rules like list_into_univ
Mon, 27 Feb 1995 17:40:57 +0100 Updated comment about list_subset_univ and list_into_univ.
lcp [Mon, 27 Feb 1995 17:40:57 +0100] rev 908
Updated comment about list_subset_univ and list_into_univ.
Mon, 27 Feb 1995 17:27:50 +0100 exit: new, for use in Makefiles
lcp [Mon, 27 Feb 1995 17:27:50 +0100] rev 907
exit: new, for use in Makefiles
Mon, 27 Feb 1995 17:11:25 +0100 Redefined arithmetic to suppress redundant leading 0s and 1s
lcp [Mon, 27 Feb 1995 17:11:25 +0100] rev 906
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.
Mon, 27 Feb 1995 17:08:51 +0100 Added integer numerals (mostly due to Markus Wenzel)
lcp [Mon, 27 Feb 1995 17:08:51 +0100] rev 905
Added integer numerals (mostly due to Markus Wenzel) renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.
Mon, 27 Feb 1995 17:06:19 +0100 Proved zadd_left_commute and zmult_left_commute to define
lcp [Mon, 27 Feb 1995 17:06:19 +0100] rev 904
Proved zadd_left_commute and zmult_left_commute to define zadd_ac and zmult_ac. Deleted add_cong, add_kill and add_left_commute_kill as unused. Defined zadd_simps, zminus_simps, zmult_simps and added them to integ_ss.
Mon, 27 Feb 1995 16:58:59 +0100 New shell script for finding orphan .ML files (those with no
lcp [Mon, 27 Feb 1995 16:58:59 +0100] rev 903
New shell script for finding orphan .ML files (those with no .thy file)
Fri, 24 Feb 1995 11:52:19 +0100 added ExcludeThm; cleaned up Makefile; fixed isalpha bug (replaced by isalnum)
clasohm [Fri, 24 Feb 1995 11:52:19 +0100] rev 902
added ExcludeThm; cleaned up Makefile; fixed isalpha bug (replaced by isalnum)
Fri, 17 Feb 1995 13:25:11 +0100 added check "length ts > 1" before printing ambiguity warning in infer_types
clasohm [Fri, 17 Feb 1995 13:25:11 +0100] rev 901
added check "length ts > 1" before printing ambiguity warning in infer_types
(0) -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip