# HG changeset patch
# User paulson
# Date 964168112 -7200
# Node ID 1c9851cdfe9f3d46f7df7fd0f476b05246021e5f
# Parent  1ff8a6234c6a7dd3d2b4b08ebe86f5b5c2296276
Univ no longer requires Arith (really it never did)

diff -r 1ff8a6234c6a -r 1c9851cdfe9f src/ZF/Univ.thy
--- a/src/ZF/Univ.thy	Thu Jul 20 12:04:47 2000 +0200
+++ b/src/ZF/Univ.thy	Fri Jul 21 10:28:32 2000 +0200
@@ -11,7 +11,7 @@
   But Ind_Syntax.univ refers to the constant "Univ.univ"
 *)
 
-Univ = Arith + Sum + Finite + mono +
+Univ = Epsilon + Sum + Finite + mono +
 
 consts
     Vfrom       :: [i,i]=>i