changeset 12546 | 0c90e581379f |
parent 12434 | ff2efde4574d |
child 13630 | a013a9dd370f |
--- a/src/HOL/IMP/Hoare.thy Tue Dec 18 21:28:01 2001 +0100 +++ b/src/HOL/IMP/Hoare.thy Wed Dec 19 00:26:04 2001 +0100 @@ -14,7 +14,7 @@ "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t" consts hoare :: "(assn * com * assn) set" -syntax "@hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50) +syntax "_hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50) translations "|- {P}c{Q}" == "(P,c,Q) : hoare" inductive hoare