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