| Thu, 03 Nov 1994 12:06:37 +0100 |
lcp |
ZF/upair/theI2: new
|
changeset |
files
|
| Thu, 03 Nov 1994 11:58:16 +0100 |
lcp |
ZF/equalities/domain_converse,range_converse,
|
changeset |
files
|
| Thu, 03 Nov 1994 11:52:04 +0100 |
lcp |
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
|
changeset |
files
|
| Thu, 03 Nov 1994 11:45:41 +0100 |
lcp |
Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
|
changeset |
files
|
| Thu, 03 Nov 1994 08:34:53 +0100 |
clasohm |
added warning message
|
changeset |
files
|
| Wed, 02 Nov 1994 12:48:22 +0100 |
lcp |
Provers/classical: now takes theorem "classical" as argument, proves "swap"
|
changeset |
files
|
| Wed, 02 Nov 1994 12:44:03 +0100 |
lcp |
Provers/hypsubst: greatly simplified! No longer simulates a
|
changeset |
files
|
| Wed, 02 Nov 1994 10:45:14 +0100 |
lcp |
Pure/sign/infer_types/exn_type_msg: new, for more uniform handling of
|
changeset |
files
|
| Wed, 02 Nov 1994 09:09:30 +0100 |
nipkow |
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
|
changeset |
files
|
| Tue, 01 Nov 1994 10:40:10 +0100 |
lcp |
FOL/FOL/swap: deleted
|
changeset |
files
|
| Tue, 01 Nov 1994 10:32:18 +0100 |
lcp |
HOLCF/Ssum3.ML: changed res_inst_tac [("P"... to res_inst_tac [("Pa" in
|
changeset |
files
|
| Mon, 31 Oct 1994 18:15:24 +0100 |
lcp |
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
|
changeset |
files
|
| Mon, 31 Oct 1994 18:11:12 +0100 |
lcp |
ZF/domrange/image_subset: tidied
|
changeset |
files
|
| Mon, 31 Oct 1994 18:09:32 +0100 |
lcp |
ZF/upair/mem_asym,succ_inject: tidied
|
changeset |
files
|
| Mon, 31 Oct 1994 18:07:29 +0100 |
lcp |
com1,2: added simplifier calls to remove use of ssubst in fast_tac
|
changeset |
files
|
| Mon, 31 Oct 1994 18:03:14 +0100 |
lcp |
Pure/tctical/THEN_ELSE: new
|
changeset |
files
|