equal
deleted
inserted
replaced
237 Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} |
237 Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} |
238 "verification condition generator" |
238 "verification condition generator" |
239 |
239 |
240 method_setup vcg_simp = {* |
240 method_setup vcg_simp = {* |
241 Scan.succeed (fn ctxt => |
241 Scan.succeed (fn ctxt => |
242 SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *} |
242 SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} |
243 "verification condition generator plus simplification" |
243 "verification condition generator plus simplification" |
244 |
244 |
245 end |
245 end |