# HG changeset patch
# User paulson
# Date 910960103 -3600
# Node ID 9be441c17f6d941ad42a375d3822897545b40739
# Parent  1f72c4233a8b87fc8ed2f302f58665ff28b48df4
the type of @evalcn was wrong

diff -r 1f72c4233a8b -r 9be441c17f6d src/HOL/IMP/Transition.thy
--- 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)