local;

--- a/src/ZF/Fixedpt.thy	Mon Oct 20 10:53:25 1997 +0200
+++ b/src/ZF/Fixedpt.thy	Mon Oct 20 10:53:42 1997 +0200
@@ -14,7 +14,7 @@
   bnd_mono    :: [i,i=>i]=>o
   lfp, gfp    :: [i,i=>i]=>i
 
-path Fixedpt
+local
 
 defs
   (*monotone operator from Pow(D) to itself*)

--- a/src/ZF/OrdQuant.thy	Mon Oct 20 10:53:25 1997 +0200
+++ b/src/ZF/OrdQuant.thy	Mon Oct 20 10:53:42 1997 +0200
@@ -32,7 +32,7 @@
   "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
   "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
 
-path OrdQuant
+local
 
 defs
   

--- a/src/ZF/QPair.thy	Mon Oct 20 10:53:25 1997 +0200
+++ b/src/ZF/QPair.thy	Mon Oct 20 10:53:42 1997 +0200
@@ -34,7 +34,7 @@
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
   "A <*> B"      => "QSigma(A, _K(B))"
 
-path QPair
+local
 
 defs
   QPair_def       "<a;b> == a+b"

--- a/src/ZF/QUniv.thy	Mon Oct 20 10:53:25 1997 +0200
+++ b/src/ZF/QUniv.thy	Mon Oct 20 10:53:42 1997 +0200
@@ -13,7 +13,7 @@
 consts
     quniv        :: i=>i
 
-path QUniv
+local
 
 defs
     quniv_def    "quniv(A) == Pow(univ(eclose(A)))"

--- a/src/ZF/Sum.thy	Mon Oct 20 10:53:25 1997 +0200
+++ b/src/ZF/Sum.thy	Mon Oct 20 10:53:42 1997 +0200
@@ -17,7 +17,7 @@
     case        :: [i=>i, i=>i, i]=>i
     Part        :: [i,i=>i] => i
 
-path Sum
+local
 
 defs
     sum_def     "A+B == {0}*A Un {1}*B"

--- a/src/ZF/Univ.thy	Mon Oct 20 10:53:25 1997 +0200
+++ b/src/ZF/Univ.thy	Mon Oct 20 10:53:42 1997 +0200
@@ -24,7 +24,7 @@
 translations
     "Vset(x)"   ==      "Vfrom(0,x)"
 
-path Univ
+local
 
 defs
     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"

--- a/src/ZF/ZF.thy	Mon Oct 20 10:53:25 1997 +0200
+++ b/src/ZF/ZF.thy	Mon Oct 20 10:53:42 1997 +0200
@@ -167,7 +167,7 @@
   succ_def      "succ(i) == cons(i, i)"
 
 
-path ZF
+local
 
 rules