src/ZF/upair.thy
author paulson
Wed Jan 27 10:31:31 1999 +0100 (1999-01-27)
changeset 6153 bff90585cce5
parent 3924 7d391943bc19
child 9570 e16e168984e1
permissions -rw-r--r--
new typechecking solver for the simplifier
paulson@2469
     1
(*  Title:      ZF/upair.thy
paulson@2469
     2
    ID:         $Id$
paulson@2469
     3
    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
paulson@2469
     4
    Copyright   1993  University of Cambridge
paulson@2469
     5
paulson@2872
     6
Dummy theory, but holds the standard ZF simpset.
paulson@2469
     7
*)
paulson@2469
     8
paulson@6153
     9
upair = ZF +
paulson@6153
    10
paulson@6153
    11
setup
paulson@6153
    12
  TypeCheck.setup
paulson@6153
    13
paulson@6153
    14
end
paulson@6153
    15