src/ZF/QUniv.thy
changeset 6112 5e4871c5136b
parent 6093 87bf8c03b169
child 13220 62c899c77151
     1.1 --- a/src/ZF/QUniv.thy	Wed Jan 13 11:56:28 1999 +0100
     1.2 +++ b/src/ZF/QUniv.thy	Wed Jan 13 11:57:09 1999 +0100
     1.3 @@ -8,8 +8,20 @@
     1.4  
     1.5  QUniv = Univ + QPair + mono + equalities +
     1.6  
     1.7 +(*Disjoint sums as a datatype*)
     1.8 +rep_datatype 
     1.9 +  elim		sumE
    1.10 +  induct	TrueI
    1.11 +  case_eqns	case_Inl, case_Inr
    1.12 +
    1.13 +(*Variant disjoint sums as a datatype*)
    1.14 +rep_datatype 
    1.15 +  elim		qsumE
    1.16 +  induct	TrueI
    1.17 +  case_eqns	qcase_QInl, qcase_QInr
    1.18 +
    1.19  constdefs
    1.20    quniv :: i => i
    1.21 -  "quniv(A) == Pow(univ(eclose(A)))"
    1.22 +   "quniv(A) == Pow(univ(eclose(A)))"
    1.23  
    1.24  end