src/HOL/IMP/Hoare.thy

--- a/src/HOL/IMP/Hoare.thy	Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/IMP/Hoare.thy	Wed Nov 29 17:01:41 1995 +0100
@@ -8,8 +8,8 @@
 
 Hoare = Denotation +
 consts
-  spec :: "[state=>bool,com,state=>bool] => bool"
-(* syntax "@spec" :: "[bool,com,bool] => bool" *)
+  spec :: [state=>bool,com,state=>bool] => bool
+(* syntax "@spec" :: [bool,com,bool] => bool *)
           ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
 defs
   spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"