equal
deleted
inserted
replaced
110 Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} |
110 Scan.succeed (fn ctxt => SIMPLE_METHOD' (hoare_tac ctxt (K all_tac))) *} |
111 "verification condition generator" |
111 "verification condition generator" |
112 |
112 |
113 method_setup vcg_simp = {* |
113 method_setup vcg_simp = {* |
114 Scan.succeed (fn ctxt => |
114 Scan.succeed (fn ctxt => |
115 SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} |
115 SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac ctxt))) *} |
116 "verification condition generator plus simplification" |
116 "verification condition generator plus simplification" |
117 |
117 |
118 (* Special syntax for guarded statements and guarded array updates: *) |
118 (* Special syntax for guarded statements and guarded array updates: *) |
119 |
119 |
120 syntax |
120 syntax |