author | wenzelm |
Sat, 15 Apr 2000 15:00:57 +0200 | |
changeset 8717 | 20c42415c07d |
parent 6153 | bff90585cce5 |
child 9570 | e16e168984e1 |
permissions | -rw-r--r-- |
2469 | 1 |
(* Title: ZF/upair.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory |
|
4 |
Copyright 1993 University of Cambridge |
|
5 |
||
2872
ac81a17f86f8
Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy
paulson
parents:
2469
diff
changeset
|
6 |
Dummy theory, but holds the standard ZF simpset. |
2469 | 7 |
*) |
8 |
||
6153 | 9 |
upair = ZF + |
10 |
||
11 |
setup |
|
12 |
TypeCheck.setup |
|
13 |
||
14 |
end |
|
15 |