equal
deleted
inserted
replaced
226 |
226 |
227 |
227 |
228 use "hoare.ML" |
228 use "hoare.ML" |
229 |
229 |
230 method_setup vcg = {* |
230 method_setup vcg = {* |
231 Method.no_args |
231 Method.no_args (Method.SIMPLE_METHOD' (hoare_tac (K all_tac))) *} |
232 (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *} |
|
233 "verification condition generator" |
232 "verification condition generator" |
234 |
233 |
235 method_setup vcg_simp = {* |
234 method_setup vcg_simp = {* |
236 Method.ctxt_args (fn ctxt => |
235 Method.ctxt_args (fn ctxt => |
237 Method.METHOD (fn facts => |
236 Method.SIMPLE_METHOD' (hoare_tac (asm_full_simp_tac (local_simpset_of ctxt)))) *} |
238 hoare_tac (asm_full_simp_tac (local_simpset_of ctxt))1)) *} |
|
239 "verification condition generator plus simplification" |
237 "verification condition generator plus simplification" |
240 |
238 |
241 end |
239 end |