local;
authorwenzelm
Mon Oct 20 10:53:42 1997 +0200 (1997-10-20)
changeset 39401d5bee4d047f
parent 3939 83f908ed3c04
child 3941 ea440c63d206
local;
src/ZF/Fixedpt.thy
src/ZF/OrdQuant.thy
src/ZF/QPair.thy
src/ZF/QUniv.thy
src/ZF/Sum.thy
src/ZF/Univ.thy
src/ZF/ZF.thy
     1.1 --- a/src/ZF/Fixedpt.thy	Mon Oct 20 10:53:25 1997 +0200
     1.2 +++ b/src/ZF/Fixedpt.thy	Mon Oct 20 10:53:42 1997 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    bnd_mono    :: [i,i=>i]=>o
     1.5    lfp, gfp    :: [i,i=>i]=>i
     1.6  
     1.7 -path Fixedpt
     1.8 +local
     1.9  
    1.10  defs
    1.11    (*monotone operator from Pow(D) to itself*)
     2.1 --- a/src/ZF/OrdQuant.thy	Mon Oct 20 10:53:25 1997 +0200
     2.2 +++ b/src/ZF/OrdQuant.thy	Mon Oct 20 10:53:42 1997 +0200
     2.3 @@ -32,7 +32,7 @@
     2.4    "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
     2.5    "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
     2.6  
     2.7 -path OrdQuant
     2.8 +local
     2.9  
    2.10  defs
    2.11    
     3.1 --- a/src/ZF/QPair.thy	Mon Oct 20 10:53:25 1997 +0200
     3.2 +++ b/src/ZF/QPair.thy	Mon Oct 20 10:53:42 1997 +0200
     3.3 @@ -34,7 +34,7 @@
     3.4    "QSUM x:A. B"  => "QSigma(A, %x. B)"
     3.5    "A <*> B"      => "QSigma(A, _K(B))"
     3.6  
     3.7 -path QPair
     3.8 +local
     3.9  
    3.10  defs
    3.11    QPair_def       "<a;b> == a+b"
     4.1 --- a/src/ZF/QUniv.thy	Mon Oct 20 10:53:25 1997 +0200
     4.2 +++ b/src/ZF/QUniv.thy	Mon Oct 20 10:53:42 1997 +0200
     4.3 @@ -13,7 +13,7 @@
     4.4  consts
     4.5      quniv        :: i=>i
     4.6  
     4.7 -path QUniv
     4.8 +local
     4.9  
    4.10  defs
    4.11      quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
     5.1 --- a/src/ZF/Sum.thy	Mon Oct 20 10:53:25 1997 +0200
     5.2 +++ b/src/ZF/Sum.thy	Mon Oct 20 10:53:42 1997 +0200
     5.3 @@ -17,7 +17,7 @@
     5.4      case        :: [i=>i, i=>i, i]=>i
     5.5      Part        :: [i,i=>i] => i
     5.6  
     5.7 -path Sum
     5.8 +local
     5.9  
    5.10  defs
    5.11      sum_def     "A+B == {0}*A Un {1}*B"
     6.1 --- a/src/ZF/Univ.thy	Mon Oct 20 10:53:25 1997 +0200
     6.2 +++ b/src/ZF/Univ.thy	Mon Oct 20 10:53:42 1997 +0200
     6.3 @@ -24,7 +24,7 @@
     6.4  translations
     6.5      "Vset(x)"   ==      "Vfrom(0,x)"
     6.6  
     6.7 -path Univ
     6.8 +local
     6.9  
    6.10  defs
    6.11      Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"
     7.1 --- a/src/ZF/ZF.thy	Mon Oct 20 10:53:25 1997 +0200
     7.2 +++ b/src/ZF/ZF.thy	Mon Oct 20 10:53:42 1997 +0200
     7.3 @@ -167,7 +167,7 @@
     7.4    succ_def      "succ(i) == cons(i, i)"
     7.5  
     7.6  
     7.7 -path ZF
     7.8 +local
     7.9  
    7.10  rules
    7.11