equal
deleted
inserted
replaced
7 |
7 |
8 NOTE: univ(A) could be a translation; would simplify many proofs! |
8 NOTE: univ(A) could be a translation; would simplify many proofs! |
9 But Ind_Syntax.univ refers to the constant "Univ.univ" |
9 But Ind_Syntax.univ refers to the constant "Univ.univ" |
10 *) |
10 *) |
11 |
11 |
12 header{*The Cumulative Hierarchy and a Small Universe for Recursive Types*} |
12 section{*The Cumulative Hierarchy and a Small Universe for Recursive Types*} |
13 |
13 |
14 theory Univ imports Epsilon Cardinal begin |
14 theory Univ imports Epsilon Cardinal begin |
15 |
15 |
16 definition |
16 definition |
17 Vfrom :: "[i,i]=>i" where |
17 Vfrom :: "[i,i]=>i" where |