isabelle: src/ZF/upair.thy@f98beaaa7c4f (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	*)
b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 124 diff changeset	6
9570 e16e168984e1 installation of cancellation simprocs for the integers paulson parents: 6153 diff changeset	7	theory upair = ZF
e16e168984e1 installation of cancellation simprocs for the integers paulson parents: 6153 diff changeset	8	files "Tools/typechk":
6153 bff90585cce5 new typechecking solver for the simplifier paulson parents: 3924 diff changeset	9
9907 473a6604da94 tuned ML code (the_context, bind_thms(s)); wenzelm parents: 9570 diff changeset	10	setup TypeCheck.setup
11770 b6bb7a853dd2 moved rulify to ObjectLogic; wenzelm parents: 9907 diff changeset	11	declare atomize_ball [symmetric, rulify]
6153 bff90585cce5 new typechecking solver for the simplifier paulson parents: 3924 diff changeset	12
bff90585cce5 new typechecking solver for the simplifier paulson parents: 3924 diff changeset	13	end

author	wenzelm
	Sat, 24 Nov 2001 16:54:32 +0100
changeset 12282	f98beaaa7c4f
parent 11770	b6bb7a853dd2
child 13259	01fa0c8dbc92
permissions	-rw-r--r--