isabelle: src/ZF/quniv.thy@9670dae0143d (annotated)

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	1	(* Title: ZF/univ.thy
a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
a5a9c433f639 Initial revision clasohm parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
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
124 858ab9a9b047 made pseudo theories for all ML files; clasohm parents: 0 diff changeset	9	QUniv = Univ + QPair + "mono" + "equalities" +
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	10	consts
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	quniv :: "i=>i"
a5a9c433f639 Initial revision clasohm parents: diff changeset	12
a5a9c433f639 Initial revision clasohm parents: diff changeset	13	rules
a5a9c433f639 Initial revision clasohm parents: diff changeset	14	quniv_def "quniv(A) == Pow(univ(eclose(A)))"
a5a9c433f639 Initial revision clasohm parents: diff changeset	15
a5a9c433f639 Initial revision clasohm parents: diff changeset	16	end