equal
deleted
inserted
replaced
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 header{*The Cumulative Hierarchy and a Small Universe for Recursive Types*} |
13 |
13 |
14 theory Univ = Epsilon + Cardinal: |
14 theory Univ imports Epsilon Cardinal begin |
15 |
15 |
16 constdefs |
16 constdefs |
17 Vfrom :: "[i,i]=>i" |
17 Vfrom :: "[i,i]=>i" |
18 "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))" |
18 "Vfrom(A,i) == transrec(i, %x f. A Un (\<Union>y\<in>x. Pow(f`y)))" |
19 |
19 |