changeset 41476 | 0fa9629aa399 |
parent 40945 | b8703f63bfb2 |
child 42151 | 4da4fc77664b |
--- a/src/HOL/HOLCF/IMP/HoareEx.thy Sat Jan 08 00:28:31 2011 +0100 +++ b/src/HOL/HOLCF/IMP/HoareEx.thy Sat Jan 08 09:30:52 2011 -0800 @@ -13,7 +13,7 @@ the correctness of the Hoare rule for while-loops. *} -types assn = "state => bool" +type_synonym assn = "state => bool" definition hoare_valid :: "[assn, com, assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where