Tue, 28 Feb 1995 10:50:37 +0100 Re-organised to perform the tests independently. Now test
lcp [Tue, 28 Feb 1995 10:50:37 +0100] rev 917
Re-organised to perform the tests independently. Now test is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to refer to the right command for running the object-logic. Uses "suffix substitution" to shorten macro definitions.
Tue, 28 Feb 1995 10:33:52 +0100 New example by Jacob Frost, tidied by lcp
lcp [Tue, 28 Feb 1995 10:33:52 +0100] rev 916
New example by Jacob Frost, tidied by lcp
Mon, 27 Feb 1995 18:12:21 +0100 New example by Jacob Frost, tidied by lcp
lcp [Mon, 27 Feb 1995 18:12:21 +0100] rev 915
New example by Jacob Frost, tidied by lcp
Mon, 27 Feb 1995 18:07:59 +0100 Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
lcp [Mon, 27 Feb 1995 18:07:59 +0100] rev 914
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.
Mon, 27 Feb 1995 18:05:38 +0100 Updated the "version" variable (which was never done for
lcp [Mon, 27 Feb 1995 18:05:38 +0100] rev 913
Updated the "version" variable (which was never done for Isabelle-94 revisions 1 and 2!)
Mon, 27 Feb 1995 17:51:12 +0100 Redefined functions to suppress redundant leading 0s and 1s
lcp [Mon, 27 Feb 1995 17:51:12 +0100] rev 912
Redefined functions to suppress redundant leading 0s and 1s
Mon, 27 Feb 1995 17:47:57 +0100 new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm [Mon, 27 Feb 1995 17:47:57 +0100] rev 911
new in mixfix annotations: "' " (quote space) separates delimiters without adding extra white space for printing;
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.
(0) -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip