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

6093 87bf8c03b169 eliminated global/local names; wenzelm parents: 3940 diff changeset	1	(* Title: ZF/QUniv.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
6093 87bf8c03b169 eliminated global/local names; wenzelm parents: 3940 diff changeset	6	A small universe for lazy recursive types.
0 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
6112 5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	11	(Disjoint sums as a datatype)
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	12	rep_datatype
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	13	elim sumE
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	14	induct TrueI
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	15	case_eqns case_Inl, case_Inr
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	16
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	17	(Variant disjoint sums as a datatype)
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	18	rep_datatype
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	19	elim qsumE
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	20	induct TrueI
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	21	case_eqns qcase_QInl, qcase_QInr
5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	22
6093 87bf8c03b169 eliminated global/local names; wenzelm parents: 3940 diff changeset	23	constdefs
87bf8c03b169 eliminated global/local names; wenzelm parents: 3940 diff changeset	24	quniv :: i => i
6112 5e4871c5136b datatype package improvements paulson parents: 6093 diff changeset	25	"quniv(A) == Pow(univ(eclose(A)))"
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	26
a5a9c433f639 Initial revision clasohm parents: diff changeset	27	end

author	paulson
	Wed, 13 Jan 1999 11:57:09 +0100
changeset 6112	5e4871c5136b
parent 6093	87bf8c03b169
child 13220	62c899c77151
permissions	-rw-r--r--