isabelle: src/ZF/upair.thy@15763781afb0 (annotated)

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.
ac81a17f86f8 Moved definitions (binary intersection, etc.) from upair.thy back to ZF.thy paulson parents: 2469 diff changeset	7	(This is why the +end is present.)
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 124 diff changeset	8	*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 124 diff changeset	9
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 124 diff changeset	10	upair = ZF +
124 858ab9a9b047 made pseudo theories for all ML files; clasohm parents: diff changeset	11
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 124 diff changeset	12	end