(* Title: ZF/upair.thy ID: $Id$ Author: Lawrence C Paulson and Martin D Coen, CU Computer Laboratory Copyright 1993 University of Cambridge Dummy theory, but holds the standard ZF simpset. (This is why the +end is present.) *) upair = ZF + end