isabelle: src/ZF/upair.thy@adda1dc18bb8 (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.
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
9570 e16e168984e1 installation of cancellation simprocs for the integers paulson parents: 6153 diff changeset	9	theory upair = ZF
e16e168984e1 installation of cancellation simprocs for the integers paulson parents: 6153 diff changeset	10	files "Tools/typechk":
6153 bff90585cce5 new typechecking solver for the simplifier paulson parents: 3924 diff changeset	11
bff90585cce5 new typechecking solver for the simplifier paulson parents: 3924 diff changeset	12	setup
bff90585cce5 new typechecking solver for the simplifier paulson parents: 3924 diff changeset	13	TypeCheck.setup
bff90585cce5 new typechecking solver for the simplifier paulson parents: 3924 diff changeset	14
bff90585cce5 new typechecking solver for the simplifier paulson parents: 3924 diff changeset	15	end
bff90585cce5 new typechecking solver for the simplifier paulson parents: 3924 diff changeset	16

author	wenzelm
	Sat, 02 Sep 2000 21:48:10 +0200
changeset 9802	adda1dc18bb8
parent 9570	e16e168984e1
child 9907	473a6604da94
permissions	-rw-r--r--