equal
deleted
inserted
replaced
73 fun axiomatize_lub_take |
73 fun axiomatize_lub_take |
74 (dbind : binding, take_const : term) |
74 (dbind : binding, take_const : term) |
75 (thy : theory) |
75 (thy : theory) |
76 : thm * theory = |
76 : thm * theory = |
77 let |
77 let |
78 val i = Free ("i", natT) |
78 val i = Free ("i", \<^Type>\<open>nat\<close>) |
79 val T = (fst o dest_cfunT o range_type o fastype_of) take_const |
79 val T = (fst o dest_cfunT o range_type o fastype_of) take_const |
80 |
80 |
81 val lub_take_eqn = |
81 val lub_take_eqn = |
82 mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T)) |
82 mk_trp (mk_eq (mk_lub (lambda i (take_const $ i)), mk_ID T)) |
83 |
83 |