equal
deleted
inserted
replaced
44 val vc_goal = concl_args |
44 val vc_goal = concl_args |
45 |> HOLogic.mk_tuple |
45 |> HOLogic.mk_tuple |
46 |> mk_fresh_star avoid_trm |
46 |> mk_fresh_star avoid_trm |
47 |> HOLogic.mk_Trueprop |
47 |> HOLogic.mk_Trueprop |
48 |> (curry Logic.list_implies) prems |
48 |> (curry Logic.list_implies) prems |
49 |> (curry list_all_free) params |
49 |> fold_rev (Logic.all o Free) params |
50 val finite_goal = avoid_trm |
50 val finite_goal = avoid_trm |
51 |> mk_finite |
51 |> mk_finite |
52 |> HOLogic.mk_Trueprop |
52 |> HOLogic.mk_Trueprop |
53 |> (curry Logic.list_implies) prems |
53 |> (curry Logic.list_implies) prems |
54 |> (curry list_all_free) params |
54 |> fold_rev (Logic.all o Free) params |
55 in |
55 in |
56 if null avoid then [] else [vc_goal, finite_goal] |
56 if null avoid then [] else [vc_goal, finite_goal] |
57 end |
57 end |
58 |
58 |
59 (* fixme: move to nominal_library *) |
59 (* fixme: move to nominal_library *) |