equal
deleted
inserted
replaced
56 |
56 |
57 fun mk_lub t = |
57 fun mk_lub t = |
58 let |
58 let |
59 val T = Term.range_type (Term.fastype_of t) |
59 val T = Term.range_type (Term.fastype_of t) |
60 val UNIV_const = \<^term>\<open>UNIV :: nat set\<close> |
60 val UNIV_const = \<^term>\<open>UNIV :: nat set\<close> |
61 in \<^Const>\<open>lub T for \<open>\<^Const>\<open>image \<open>\<^Type>\<open>nat\<close>\<close> T for t UNIV_const\<close>\<close>\<close> end |
61 in \<^Const>\<open>lub T for \<^Const>\<open>image \<^Type>\<open>nat\<close> T for t UNIV_const\<close>\<close> end |
62 |
62 |
63 |
63 |
64 (*** Continuous function space ***) |
64 (*** Continuous function space ***) |
65 |
65 |
66 fun mk_cfunT (T, U) = \<^Type>\<open>cfun T U\<close> |
66 fun mk_cfunT (T, U) = \<^Type>\<open>cfun T U\<close> |