equal
deleted
inserted
replaced
37 apply (fast elim: fun_weaken_type) |
37 apply (fast elim: fun_weaken_type) |
38 apply (fast dest: apply_type) |
38 apply (fast dest: apply_type) |
39 done |
39 done |
40 |
40 |
41 |
41 |
42 subsection {* The Martin-Löf wellordering type *} |
42 subsection {* The Martin-Löf wellordering type *} |
43 |
43 |
44 consts |
44 consts |
45 Well :: "[i, i => i] => i" |
45 Well :: "[i, i => i] => i" |
46 |
46 |
47 datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))" |
47 datatype \<subseteq> "Vfrom(A \<union> (\<Union>x \<in> A. B(x)), csucc(nat \<union> |\<Union>x \<in> A. B(x)|))" |