equal
deleted
inserted
replaced
104 val concl = |
104 val concl = |
105 HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj}) |
105 HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name HOL.conj}) |
106 (map (fn ((((i, _), T), U), tname) => |
106 (map (fn ((((i, _), T), U), tname) => |
107 make_pred i U T (mk_proj i is r) (Free (tname, T))) |
107 make_pred i U T (mk_proj i is r) (Free (tname, T))) |
108 (descr ~~ recTs ~~ rec_result_Ts ~~ tnames))); |
108 (descr ~~ recTs ~~ rec_result_Ts ~~ tnames))); |
109 val inst = map (pairself cert) (map head_of (HOLogic.dest_conj |
109 val inst = map (apply2 cert) (map head_of (HOLogic.dest_conj |
110 (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps); |
110 (HOLogic.dest_Trueprop (concl_of induct))) ~~ ps); |
111 |
111 |
112 val thm = |
112 val thm = |
113 Goal.prove_internal ctxt (map cert prems) (cert concl) |
113 Goal.prove_internal ctxt (map cert prems) (cert concl) |
114 (fn prems => |
114 (fn prems => |