src/HOL/IMP/Hoare.thy
changeset 4897 be11be0b6ea1
parent 3842 b55686a7b22c
child 5102 8c782c25a11e
     1.1 --- a/src/HOL/IMP/Hoare.thy	Tue May 05 17:28:22 1998 +0200
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Wed May 06 11:46:00 1998 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  inductive hoare
     1.5  intrs
     1.6    skip "|- {P}SKIP{P}"
     1.7 -  ass  "|- {%s. P(s[a s/x])} x:=a {P}"
     1.8 +  ass  "|- {%s. P(s[x:=a s])} x:=a {P}"
     1.9    semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
    1.10    If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
    1.11        |- {P} IF b THEN c ELSE d {Q}"