equal
deleted
inserted
replaced
67 st |
67 st |
68 |> ALLGOALS (CONVERSION drop_assert_at) |
68 |> ALLGOALS (CONVERSION drop_assert_at) |
69 |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #> |
69 |> Seq.map (pair (map (rpair [] o case_name_of) (Thm.prems_of st)))) #> |
70 Seq.maps (fn (names, st) => |
70 Seq.maps (fn (names, st) => |
71 CASES |
71 CASES |
72 (Rule_Cases.make_common false |
72 (Rule_Cases.make_common |
73 (ProofContext.theory_of ctxt, Thm.prop_of st) names) |
73 (ProofContext.theory_of ctxt, |
|
74 Thm.prop_of (Rule_Cases.internalize_params st)) names) |
74 Tactical.all_tac st)) |
75 Tactical.all_tac st)) |
75 in |
76 in |
76 val setup_boogie_cases = Method.setup @{binding boogie_cases} |
77 val setup_boogie_cases = Method.setup @{binding boogie_cases} |
77 (Scan.succeed boogie_cases) |
78 (Scan.succeed boogie_cases) |
78 "Prepares a set of Boogie assertions for case-based proofs" |
79 "Prepares a set of Boogie assertions for case-based proofs" |