isabelle: src/ZF/QUniv.thy@e00ac9db9975 (annotated)

1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	1	(* Title: ZF/univ.thy
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1478 2b8c2a7547ab expanded tabs clasohm parents: 1401 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1993 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	A small universe for lazy recursive types
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	8
2469 b50b8c0eec01 Implicit simpsets and clasets for FOL and ZF paulson parents: 1478 diff changeset	9	QUniv = Univ + QPair + mono + equalities +
3923 c257b82a1200 global; wenzelm parents: 2469 diff changeset	10
c257b82a1200 global; wenzelm parents: 2469 diff changeset	11	global
c257b82a1200 global; wenzelm parents: 2469 diff changeset	12
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	13	consts
1401 0c439768f45c removed quotes from consts and syntax sections clasohm parents: 753 diff changeset	14	quniv :: i=>i
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	15
3940 1d5bee4d047f local; wenzelm parents: 3923 diff changeset	16	local
3923 c257b82a1200 global; wenzelm parents: 2469 diff changeset	17
753 ec86863e87c8 replaced "rules" by "defs" lcp parents: 124 diff changeset	18	defs
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	19	quniv_def "quniv(A) == Pow(univ(eclose(A)))"
a5a9c433f639 Initial revision clasohm parents: diff changeset	20
a5a9c433f639 Initial revision clasohm parents: diff changeset	21	end

author	wenzelm
	Sat, 13 Jun 1998 18:25:39 +0200
changeset 5036	e00ac9db9975
parent 3940	1d5bee4d047f
child 6093	87bf8c03b169
permissions	-rw-r--r--