src/ZF/upair.thy
author wenzelm
Sat, 15 Apr 2000 15:00:57 +0200
changeset 8717 20c42415c07d
parent 6153 bff90585cce5
child 9570 e16e168984e1
permissions -rw-r--r--
plain ASCII;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2469
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
     1
(*  Title:      ZF/upair.thy
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
     2
    ID:         $Id$
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
     3
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
     4
    Copyright   1993  University of Cambridge
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
     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
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
     7
*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF
paulson
parents: 124
diff changeset
     8
6153
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 3924
diff changeset
     9
upair = ZF +
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 3924
diff changeset
    10
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 3924
diff changeset
    11
setup
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 3924
diff changeset
    12
  TypeCheck.setup
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 3924
diff changeset
    13
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 3924
diff changeset
    14
end
bff90585cce5 new typechecking solver for the simplifier
paulson
parents: 3924
diff changeset
    15