global;
authorwenzelm
Fri Oct 17 17:40:02 1997 +0200 (1997-10-17 ago)
changeset 3923c257b82a1200
parent 3922 ca23ee574faa
child 3924 7d391943bc19
global;
src/ZF/Fixedpt.thy
src/ZF/OrdQuant.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Sum.thy
src/ZF/Univ.thy
     1.1 --- a/src/ZF/Fixedpt.thy	Fri Oct 17 17:39:04 1997 +0200
     1.2 +++ b/src/ZF/Fixedpt.thy	Fri Oct 17 17:40:02 1997 +0200
     1.3 @@ -7,10 +7,15 @@
     1.4  *)
     1.5  
     1.6  Fixedpt = domrange +
     1.7 +
     1.8 +global
     1.9 +
    1.10  consts
    1.11    bnd_mono    :: [i,i=>i]=>o
    1.12    lfp, gfp    :: [i,i=>i]=>i
    1.13  
    1.14 +path Fixedpt
    1.15 +
    1.16  defs
    1.17    (*monotone operator from Pow(D) to itself*)
    1.18    bnd_mono_def 
     2.1 --- a/src/ZF/OrdQuant.thy	Fri Oct 17 17:39:04 1997 +0200
     2.2 +++ b/src/ZF/OrdQuant.thy	Fri Oct 17 17:40:02 1997 +0200
     2.3 @@ -7,6 +7,8 @@
     2.4  
     2.5  OrdQuant = Ordinal +
     2.6  
     2.7 +global
     2.8 +
     2.9  consts
    2.10    
    2.11    (* Ordinal Quantifiers *)
    2.12 @@ -30,6 +32,7 @@
    2.13    "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
    2.14    "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
    2.15  
    2.16 +path OrdQuant
    2.17  
    2.18  defs
    2.19    
     3.1 --- a/src/ZF/QPair.thy	Fri Oct 17 17:39:04 1997 +0200
     3.2 +++ b/src/ZF/QPair.thy	Fri Oct 17 17:40:02 1997 +0200
     3.3 @@ -12,6 +12,9 @@
     3.4  *)
     3.5  
     3.6  QPair = Sum +
     3.7 +
     3.8 +global
     3.9 +
    3.10  consts
    3.11    QPair     :: [i, i] => i                      ("<(_;/ _)>")
    3.12    qfst,qsnd :: i => i
    3.13 @@ -31,6 +34,8 @@
    3.14    "QSUM x:A. B"  => "QSigma(A, %x. B)"
    3.15    "A <*> B"      => "QSigma(A, _K(B))"
    3.16  
    3.17 +path QPair
    3.18 +
    3.19  defs
    3.20    QPair_def       "<a;b> == a+b"
    3.21    qfst_def        "qfst(p) == THE a. EX b. p=<a;b>"
     4.1 --- a/src/ZF/QUniv.thy	Fri Oct 17 17:39:04 1997 +0200
     4.2 +++ b/src/ZF/QUniv.thy	Fri Oct 17 17:40:02 1997 +0200
     4.3 @@ -7,9 +7,14 @@
     4.4  *)
     4.5  
     4.6  QUniv = Univ + QPair + mono + equalities +
     4.7 +
     4.8 +global
     4.9 +
    4.10  consts
    4.11      quniv        :: i=>i
    4.12  
    4.13 +path QUniv
    4.14 +
    4.15  defs
    4.16      quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
    4.17  
     5.1 --- a/src/ZF/Sum.thy	Fri Oct 17 17:39:04 1997 +0200
     5.2 +++ b/src/ZF/Sum.thy	Fri Oct 17 17:40:02 1997 +0200
     5.3 @@ -8,12 +8,17 @@
     5.4  *)
     5.5  
     5.6  Sum = Bool + pair + 
     5.7 +
     5.8 +global
     5.9 +
    5.10  consts
    5.11      "+"         :: [i,i]=>i                     (infixr 65)
    5.12      Inl,Inr     :: i=>i
    5.13      case        :: [i=>i, i=>i, i]=>i
    5.14      Part        :: [i,i=>i] => i
    5.15  
    5.16 +path Sum
    5.17 +
    5.18  defs
    5.19      sum_def     "A+B == {0}*A Un {1}*B"
    5.20      Inl_def     "Inl(a) == <0,a>"
     6.1 --- a/src/ZF/Univ.thy	Fri Oct 17 17:39:04 1997 +0200
     6.2 +++ b/src/ZF/Univ.thy	Fri Oct 17 17:40:02 1997 +0200
     6.3 @@ -12,6 +12,9 @@
     6.4  *)
     6.5  
     6.6  Univ = Arith + Sum + Finite + mono +
     6.7 +
     6.8 +global
     6.9 +
    6.10  consts
    6.11      Vfrom       :: [i,i]=>i
    6.12      Vset        :: i=>i
    6.13 @@ -21,6 +24,8 @@
    6.14  translations
    6.15      "Vset(x)"   ==      "Vfrom(0,x)"
    6.16  
    6.17 +path Univ
    6.18 +
    6.19  defs
    6.20      Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
    6.21