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