--- 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