isabelle: src/ZF/Constructible/ROOT.ML@0f89104dd377 (annotated)

13245 714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	1	(* Title: ZF/Constructible/ROOT.ML
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	2	ID: $Id$
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	4	Copyright 2002 University of Cambridge
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	5
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	6	Inner Models and Absoluteness
13323 2c287f50c9f3 More relativization, reflection and proofs of separation paulson parents: 13306 diff changeset	7
2c287f50c9f3 More relativization, reflection and proofs of separation paulson parents: 13306 diff changeset	8	Build using isatool usedir -d pdf ZF Constructible
13245 714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	9	*)
714f7a423a15 development and tweaks paulson parents: 13223 diff changeset	10
13223 45be08fbdcff new theory of inner models paulson parents: diff changeset	11	use_thy "Reflection";
13254 5146ccaedf42 class quantifiers (some) paulson parents: 13245 diff changeset	12	use_thy "WF_absolute";
13339 0f89104dd377 Fixed quantified variable name preservation for ball and bex (bounded quants) paulson parents: 13323 diff changeset	13	use_thy "Rec_Separation";
13268 240509babf00 more use of relativized quantifiers paulson parents: 13254 diff changeset	14	use_thy "Datatype_absolute";

author	paulson
	Wed, 10 Jul 2002 16:54:07 +0200
changeset 13339	0f89104dd377
parent 13323	2c287f50c9f3
child 13494	1c44289716ae
permissions	-rw-r--r--