src/HOL/IMP/Hoare.thy
changeset 972 e61b058d58d2
parent 939 534955033ed2
child 1374 5e407f2a3323
     1.1 --- a/src/HOL/IMP/Hoare.thy	Thu Mar 23 15:39:13 1995 +0100
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Fri Mar 24 12:30:35 1995 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  (* syntax "@spec" :: "[bool,com,bool] => bool" *)
     1.5            ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
     1.6  defs
     1.7 -  spec_def "spec P c Q == !s t. <s,t> : C(c) --> P s --> Q t"
     1.8 +  spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
     1.9  end
    1.10  (* Pretty-printing of assertions.
    1.11     Not very helpful as long as programs are not pretty-printed.