equal
deleted
inserted
replaced
6 The cumulative hierarchy and a small universe for recursive types |
6 The cumulative hierarchy and a small universe for recursive types |
7 |
7 |
8 Standard notation for Vset(i) is V(i), but users might want V for a variable |
8 Standard notation for Vset(i) is V(i), but users might want V for a variable |
9 *) |
9 *) |
10 |
10 |
11 Univ = Arith + Sum + "mono" + |
11 Univ = Arith + Sum + Fin + "mono" + |
12 consts |
12 consts |
13 Vfrom :: "[i,i]=>i" |
13 Vfrom :: "[i,i]=>i" |
14 Vset :: "i=>i" |
14 Vset :: "i=>i" |
15 Vrec :: "[i, [i,i]=>i] =>i" |
15 Vrec :: "[i, [i,i]=>i] =>i" |
16 univ :: "i=>i" |
16 univ :: "i=>i" |