changeset 490 | e6f0214ddac3 |
parent 435 | ca5356bd315a |
child 516 | 1957113f0d7d |
--- a/src/ZF/Univ.thy Wed Jul 27 16:03:16 1994 +0200 +++ b/src/ZF/Univ.thy Wed Jul 27 16:09:14 1994 +0200 @@ -8,7 +8,7 @@ Standard notation for Vset(i) is V(i), but users might want V for a variable *) -Univ = Arith + Sum + "mono" + +Univ = Arith + Sum + Fin + "mono" + consts Vfrom :: "[i,i]=>i" Vset :: "i=>i"