src/HOL/IMP/Hoare.thy
changeset 1374 5e407f2a3323
parent 972 e61b058d58d2
child 1447 bc2c0acbbf29
     1.1 --- a/src/HOL/IMP/Hoare.thy	Wed Nov 29 16:58:30 1995 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Wed Nov 29 17:01:41 1995 +0100
     1.3 @@ -8,8 +8,8 @@
     1.4  
     1.5  Hoare = Denotation +
     1.6  consts
     1.7 -  spec :: "[state=>bool,com,state=>bool] => bool"
     1.8 -(* syntax "@spec" :: "[bool,com,bool] => bool" *)
     1.9 +  spec :: [state=>bool,com,state=>bool] => bool
    1.10 +(* syntax "@spec" :: [bool,com,bool] => bool *)
    1.11            ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
    1.12  defs
    1.13    spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"