isabelle: Changelog

paulson [Tue, 20 Aug 1996 12:32:16 +0200] rev 1925

Some tidying. This brittle proof depends upon AddSEs [less_SucE];

paulson [Tue, 20 Aug 1996 12:23:13 +0200] rev 1924

Corrected for new classical reasoner: redundant rules are now ignored, even if this could increase their priority

nipkow [Mon, 19 Aug 1996 15:35:11 +0200] rev 1923

updated html-link

paulson [Mon, 19 Aug 1996 13:06:30 +0200] rev 1922

Installation of auto_tac; re-organization

paulson [Mon, 19 Aug 1996 13:03:17 +0200] rev 1921

Tidied up the proofs

paulson [Mon, 19 Aug 1996 11:51:39 +0200] rev 1920

Added impOfSubs

paulson [Mon, 19 Aug 1996 11:49:31 +0200] rev 1919

Now less_zeroE is a Safe Elim rule

paulson [Mon, 19 Aug 1996 11:33:08 +0200] rev 1918

Improved comment

paulson [Mon, 19 Aug 1996 11:25:04 +0200] rev 1917

Added proof of Un_insert_right

paulson [Mon, 19 Aug 1996 11:23:25 +0200] rev 1916

Changed precedences to remove ambiguities in r^+ notation

isabelle