Thu, 03 Nov 1994 12:06:37 +0100 ZF/upair/theI2: new
lcp [Thu, 03 Nov 1994 12:06:37 +0100] rev 686
ZF/upair/theI2: new
Thu, 03 Nov 1994 11:58:16 +0100 ZF/equalities/domain_converse,range_converse,
lcp [Thu, 03 Nov 1994 11:58:16 +0100] rev 685
ZF/equalities/domain_converse,range_converse, prod_Un_distrib2,prod_Int_distrib2: new
Thu, 03 Nov 1994 11:52:04 +0100 ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
lcp [Thu, 03 Nov 1994 11:52:04 +0100] rev 684
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
Thu, 03 Nov 1994 11:45:41 +0100 Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
lcp [Thu, 03 Nov 1994 11:45:41 +0100] rev 683
Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
Thu, 03 Nov 1994 08:34:53 +0100 added warning message
clasohm [Thu, 03 Nov 1994 08:34:53 +0100] rev 682
added warning message "Currently parsed expression could be extremely ambiguous."
Wed, 02 Nov 1994 12:48:22 +0100 Provers/classical: now takes theorem "classical" as argument, proves "swap"
lcp [Wed, 02 Nov 1994 12:48:22 +0100] rev 681
Provers/classical: now takes theorem "classical" as argument, proves "swap" Provers/classical/depth_tac,deepen_tac: new
Wed, 02 Nov 1994 12:44:03 +0100 Provers/hypsubst: greatly simplified! No longer simulates a
lcp [Wed, 02 Nov 1994 12:44:03 +0100] rev 680
Provers/hypsubst: greatly simplified! No longer simulates a "eres_inst_tac" using rev_cut_eq; instead simply rotates the chosen equality to the end!
Wed, 02 Nov 1994 10:45:14 +0100 Pure/sign/infer_types/exn_type_msg: new, for more uniform handling of
lcp [Wed, 02 Nov 1994 10:45:14 +0100] rev 679
Pure/sign/infer_types/exn_type_msg: new, for more uniform handling of exception TYPE
Wed, 02 Nov 1994 09:09:30 +0100 Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow [Wed, 02 Nov 1994 09:09:30 +0100] rev 678
Modified pattern.ML to perform proper matching of Higher-Order Patterns. Modified thm.ML to preserve bound var names during rewriting. Renamed eta_matches to matches.
Tue, 01 Nov 1994 10:40:10 +0100 FOL/FOL/swap: deleted
lcp [Tue, 01 Nov 1994 10:40:10 +0100] rev 677
FOL/FOL/swap: deleted FOL/FOL: tidied the signature
(0) -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip