src/HOLCF/IMP/HoareEx.thy
changeset 10835 f4745d77e620
parent 3664 2dced1ac2d8e
child 12431 07ec657249e5
     1.1 --- a/src/HOLCF/IMP/HoareEx.thy	Tue Jan 09 15:32:27 2001 +0100
     1.2 +++ b/src/HOLCF/IMP/HoareEx.thy	Tue Jan 09 15:36:30 2001 +0100
     1.3 @@ -13,6 +13,6 @@
     1.4  types assn = state => bool
     1.5  
     1.6  constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50)
     1.7 - "|= {A} c {B} == !s t. A s & D c `(Discr s) = Def t --> B t"
     1.8 + "|= {A} c {B} == !s t. A s & D c $(Discr s) = Def t --> B t"
     1.9  
    1.10  end