lcp [Tue, 28 Feb 1995 10:51:52 +0100] rev 918
Uses "suffix substitution" to shorten macro definitions.
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.
lcp [Tue, 28 Feb 1995 10:33:52 +0100] rev 916
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
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.
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!)
lcp [Mon, 27 Feb 1995 17:51:12 +0100] rev 912
Redefined functions to suppress redundant leading 0s and 1s