55 "" :: "id => vars" ("_") |
55 "" :: "id => vars" ("_") |
56 "_vars" :: "[id, vars] => vars" ("_ _") |
56 "_vars" :: "[id, vars] => vars" ("_ _") |
57 |
57 |
58 syntax |
58 syntax |
59 "@hoare_vars" :: "[vars, 'a assn,'a com,'a assn] => bool" |
59 "@hoare_vars" :: "[vars, 'a assn,'a com,'a assn] => bool" |
60 ("|- VARS _.// {_} // _ // {_}" [0,0,55,0] 50) |
60 ("VARS _// {_} // _ // {_}" [0,0,55,0] 50) |
61 syntax ("" output) |
61 syntax ("" output) |
62 "@hoare" :: "['a assn,'a com,'a assn] => bool" |
62 "@hoare" :: "['a assn,'a com,'a assn] => bool" |
63 ("|- {_} // _ // {_}" [0,55,0] 50) |
63 ("{_} // _ // {_}" [0,55,0] 50) |
64 |
64 |
65 (** parse translations **) |
65 (** parse translations **) |
66 |
66 |
67 ML{* |
67 ML{* |
68 fun mk_abstuple [] body = absfree ("x", dummyT, body) |
68 fun mk_abstuple [] body = absfree ("x", dummyT, body) |