Tue, 18 Mar 1997 15:12:53 +0100 gensym no longer generates random identifiers, but just enumerates them
paulson [Tue, 18 Mar 1997 15:12:53 +0100] rev 2806
gensym no longer generates random identifiers, but just enumerates them starting from A. The random number generator was needlessly slow and caused portability problems.
Tue, 18 Mar 1997 15:11:02 +0100 Made the indentation rational
paulson [Tue, 18 Mar 1997 15:11:02 +0100] rev 2805
Made the indentation rational
Tue, 18 Mar 1997 14:35:10 +0100 fixed Tools path;
wenzelm [Tue, 18 Mar 1997 14:35:10 +0100] rev 2804
fixed Tools path;
Tue, 18 Mar 1997 10:43:29 +0100 Conducted the IFOL proofs using intuitionistic tools
paulson [Tue, 18 Mar 1997 10:43:29 +0100] rev 2803
Conducted the IFOL proofs using intuitionistic tools
Tue, 18 Mar 1997 10:42:08 +0100 Stopped giving Introduction rules as Elimination rules
paulson [Tue, 18 Mar 1997 10:42:08 +0100] rev 2802
Stopped giving Introduction rules as Elimination rules
Tue, 18 Mar 1997 08:43:26 +0100 Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
nipkow [Tue, 18 Mar 1997 08:43:26 +0100] rev 2801
Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
Tue, 18 Mar 1997 08:42:18 +0100 Added P&P&Q = P&Q and P|P|Q = P|Q.
nipkow [Tue, 18 Mar 1997 08:42:18 +0100] rev 2800
Added P&P&Q = P&Q and P|P|Q = P|Q.
Mon, 17 Mar 1997 15:38:26 +0100 *** empty log message ***
nipkow [Mon, 17 Mar 1997 15:38:26 +0100] rev 2799
*** empty log message ***
Mon, 17 Mar 1997 15:37:41 +0100 The HOLCF-based den. sem. of IMP.
nipkow [Mon, 17 Mar 1997 15:37:41 +0100] rev 2798
The HOLCF-based den. sem. of IMP.
Mon, 17 Mar 1997 15:37:16 +0100 Added the HOLCF-based den. sem. of IMP.
nipkow [Mon, 17 Mar 1997 15:37:16 +0100] rev 2797
Added the HOLCF-based den. sem. of IMP.
(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip