equal
deleted
inserted
replaced
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
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 |
|
10 NOTE: univ(A) could be a translation; would simplify many proofs! |
|
11 But Ind_Syntax.univ refers to the constant "univ" |
9 *) |
12 *) |
10 |
13 |
11 Univ = Arith + Sum + Fin + "mono" + |
14 Univ = Arith + Sum + "mono" + |
12 consts |
15 consts |
13 Vfrom :: "[i,i]=>i" |
16 Vfrom :: "[i,i]=>i" |
14 Vset :: "i=>i" |
17 Vset :: "i=>i" |
15 Vrec :: "[i, [i,i]=>i] =>i" |
18 Vrec :: "[i, [i,i]=>i] =>i" |
16 univ :: "i=>i" |
19 univ :: "i=>i" |