Wed, 05 Mar 1997 10:05:32 +0100 HOL: renaming of "not"
paulson [Wed, 05 Mar 1997 10:05:32 +0100] rev 2726
HOL: renaming of "not"
Wed, 05 Mar 1997 10:04:45 +0100 Declares eta_contract_atom; fixed comment; some tidying
paulson [Wed, 05 Mar 1997 10:04:45 +0100] rev 2725
Declares eta_contract_atom; fixed comment; some tidying
Wed, 05 Mar 1997 10:03:30 +0100 Added comment
paulson [Wed, 05 Mar 1997 10:03:30 +0100] rev 2724
Added comment
Wed, 05 Mar 1997 10:02:53 +0100 Now declares needs_filtered_use, but still unusable with current MLWorks
paulson [Wed, 05 Mar 1997 10:02:53 +0100] rev 2723
Now declares needs_filtered_use, but still unusable with current MLWorks
Wed, 05 Mar 1997 10:01:57 +0100 Now uses rotate_tac and eta_contract_atom for greater speed
paulson [Wed, 05 Mar 1997 10:01:57 +0100] rev 2722
Now uses rotate_tac and eta_contract_atom for greater speed
Wed, 05 Mar 1997 09:59:55 +0100 New version of InterE, like its ZF counterpart
paulson [Wed, 05 Mar 1997 09:59:55 +0100] rev 2721
New version of InterE, like its ZF counterpart
Wed, 05 Mar 1997 09:59:24 +0100 Renamed constant "not" to "Not"
paulson [Wed, 05 Mar 1997 09:59:24 +0100] rev 2720
Renamed constant "not" to "Not"
Tue, 04 Mar 1997 10:58:29 +0100 Renamed constant "not" to "Not"
paulson [Tue, 04 Mar 1997 10:58:29 +0100] rev 2719
Renamed constant "not" to "Not"
Tue, 04 Mar 1997 10:48:36 +0100 Renamed constant "not" to "Not"
paulson [Tue, 04 Mar 1997 10:48:36 +0100] rev 2718
Renamed constant "not" to "Not"
Tue, 04 Mar 1997 10:42:28 +0100 best_tac avoids looping with change to RepFun_eqI in claset
paulson [Tue, 04 Mar 1997 10:42:28 +0100] rev 2717
best_tac avoids looping with change to RepFun_eqI in claset
(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip