equal
deleted
inserted
replaced
8 following Mike Gordon) would suffice. Maybe the datatype com comes in useful |
8 following Mike Gordon) would suffice. Maybe the datatype com comes in useful |
9 later. |
9 later. |
10 *) |
10 *) |
11 |
11 |
12 theory Hoare = Main |
12 theory Hoare = Main |
13 files ("Hoare.ML"): |
13 files ("hoare.ML"): |
14 |
14 |
15 types |
15 types |
16 'a bexp = "'a set" |
16 'a bexp = "'a set" |
17 'a assn = "'a set" |
17 'a assn = "'a set" |
18 |
18 |
191 Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q |
191 Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q |
192 *} |
192 *} |
193 |
193 |
194 print_translation {* [("Valid", spec_tr')] *} |
194 print_translation {* [("Valid", spec_tr')] *} |
195 |
195 |
196 use "Hoare.ML" |
196 use "hoare.ML" |
197 |
197 |
198 method_setup vcg = {* |
198 method_setup vcg = {* |
199 Method.no_args |
199 Method.no_args |
200 (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *} |
200 (Method.SIMPLE_METHOD' HEADGOAL (hoare_tac (K all_tac))) *} |
201 "verification condition generator" |
201 "verification condition generator" |