equal
deleted
inserted
replaced
19 |
19 |
20 fun mk_supports_goal ctxt qtrm = |
20 fun mk_supports_goal ctxt qtrm = |
21 let |
21 let |
22 val vs = fresh_args ctxt qtrm |
22 val vs = fresh_args ctxt qtrm |
23 val rhs = list_comb (qtrm, vs) |
23 val rhs = list_comb (qtrm, vs) |
24 val lhs = mk_supp (foldl1 HOLogic.mk_prod vs) |
24 val lhs = fold (curry HOLogic.mk_prod) vs @{term "()"} |
|
25 |> mk_supp |
25 in |
26 in |
26 mk_supports lhs rhs |
27 mk_supports lhs rhs |
27 |> HOLogic.mk_Trueprop |
28 |> HOLogic.mk_Trueprop |
28 end |
29 end |
29 |
30 |