equal
deleted
inserted
replaced
9 |
9 |
10 NOTE: univ(A) could be a translation; would simplify many proofs! |
10 NOTE: univ(A) could be a translation; would simplify many proofs! |
11 But Ind_Syntax.univ refers to the constant "univ" |
11 But Ind_Syntax.univ refers to the constant "univ" |
12 *) |
12 *) |
13 |
13 |
14 Univ = Arith + Sum + Finite + "mono" + |
14 Univ = Arith + Sum + Finite + mono + |
15 consts |
15 consts |
16 Vfrom :: [i,i]=>i |
16 Vfrom :: [i,i]=>i |
17 Vset :: i=>i |
17 Vset :: i=>i |
18 Vrec :: [i, [i,i]=>i] =>i |
18 Vrec :: [i, [i,i]=>i] =>i |
19 univ :: i=>i |
19 univ :: i=>i |