changeset 5855 | 9be441c17f6d |
parent 4906 | 0537ee95d004 |
child 8029 | 05446a898852 |
--- a/src/HOL/IMP/Transition.thy Fri Nov 13 13:27:46 1998 +0100 +++ b/src/HOL/IMP/Transition.thy Fri Nov 13 13:28:23 1998 +0100 @@ -13,7 +13,7 @@ syntax "@evalc1" :: "[(com*state),(com*state)] => bool" ("_ -1-> _" [81,81] 100) - "@evalcn" :: "[(com*state),(com*state)] => nat => bool" + "@evalcn" :: "[(com*state),nat,(com*state)] => bool" ("_ -_-> _" [81,81] 100) "@evalc*" :: "[(com*state),(com*state)] => bool" ("_ -*-> _" [81,81] 100)