Tue, 18 Mar 1997 15:15:01 +0100 A more explicit prefix because gensym now generates easily predicatable
paulson [Tue, 18 Mar 1997 15:15:01 +0100] rev 2807
A more explicit prefix because gensym now generates easily predicatable identifiers
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
(0) -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip