src/HOL/HOLCF/IMP/HoareEx.thy
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