# HG changeset patch
# User wenzelm
# Date 877102802 -7200
# Node ID c257b82a1200b0736fcb798fa6844a990a408680
# Parent  ca23ee574faa4cd581e9faa7696be7fe515196c2
global;

diff -r ca23ee574faa -r c257b82a1200 src/ZF/Fixedpt.thy
--- a/src/ZF/Fixedpt.thy	Fri Oct 17 17:39:04 1997 +0200
+++ b/src/ZF/Fixedpt.thy	Fri Oct 17 17:40:02 1997 +0200
@@ -7,10 +7,15 @@
 *)
 
 Fixedpt = domrange +
+
+global
+
 consts
   bnd_mono    :: [i,i=>i]=>o
   lfp, gfp    :: [i,i=>i]=>i
 
+path Fixedpt
+
 defs
   (*monotone operator from Pow(D) to itself*)
   bnd_mono_def 
diff -r ca23ee574faa -r c257b82a1200 src/ZF/OrdQuant.thy
--- a/src/ZF/OrdQuant.thy	Fri Oct 17 17:39:04 1997 +0200
+++ b/src/ZF/OrdQuant.thy	Fri Oct 17 17:40:02 1997 +0200
@@ -7,6 +7,8 @@
 
 OrdQuant = Ordinal +
 
+global
+
 consts
   
   (* Ordinal Quantifiers *)
@@ -30,6 +32,7 @@
   "@oex"      :: [idt, i, o] => o        ("(3\\<exists> _<_./ _)" 10)
   "@OUNION"   :: [idt, i, i] => i        ("(3\\<Union> _<_./ _)" 10)
 
+path OrdQuant
 
 defs
   
diff -r ca23ee574faa -r c257b82a1200 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Fri Oct 17 17:39:04 1997 +0200
+++ b/src/ZF/QPair.thy	Fri Oct 17 17:40:02 1997 +0200
@@ -12,6 +12,9 @@
 *)
 
 QPair = Sum +
+
+global
+
 consts
   QPair     :: [i, i] => i                      ("<(_;/ _)>")
   qfst,qsnd :: i => i
@@ -31,6 +34,8 @@
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
   "A <*> B"      => "QSigma(A, _K(B))"
 
+path QPair
+
 defs
   QPair_def       "<a;b> == a+b"
   qfst_def        "qfst(p) == THE a. EX b. p=<a;b>"
diff -r ca23ee574faa -r c257b82a1200 src/ZF/QUniv.thy
--- a/src/ZF/QUniv.thy	Fri Oct 17 17:39:04 1997 +0200
+++ b/src/ZF/QUniv.thy	Fri Oct 17 17:40:02 1997 +0200
@@ -7,9 +7,14 @@
 *)
 
 QUniv = Univ + QPair + mono + equalities +
+
+global
+
 consts
     quniv        :: i=>i
 
+path QUniv
+
 defs
     quniv_def    "quniv(A) == Pow(univ(eclose(A)))"
 
diff -r ca23ee574faa -r c257b82a1200 src/ZF/Sum.thy
--- a/src/ZF/Sum.thy	Fri Oct 17 17:39:04 1997 +0200
+++ b/src/ZF/Sum.thy	Fri Oct 17 17:40:02 1997 +0200
@@ -8,12 +8,17 @@
 *)
 
 Sum = Bool + pair + 
+
+global
+
 consts
     "+"         :: [i,i]=>i                     (infixr 65)
     Inl,Inr     :: i=>i
     case        :: [i=>i, i=>i, i]=>i
     Part        :: [i,i=>i] => i
 
+path Sum
+
 defs
     sum_def     "A+B == {0}*A Un {1}*B"
     Inl_def     "Inl(a) == <0,a>"
diff -r ca23ee574faa -r c257b82a1200 src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Fri Oct 17 17:39:04 1997 +0200
+++ b/src/ZF/Univ.thy	Fri Oct 17 17:40:02 1997 +0200
@@ -12,6 +12,9 @@
 *)
 
 Univ = Arith + Sum + Finite + mono +
+
+global
+
 consts
     Vfrom       :: [i,i]=>i
     Vset        :: i=>i
@@ -21,6 +24,8 @@
 translations
     "Vset(x)"   ==      "Vfrom(0,x)"
 
+path Univ
+
 defs
     Vfrom_def   "Vfrom(A,i) == transrec(i, %x f. A Un (UN y:x. Pow(f`y)))"