src/HOL/IMP/Hoare.thy
changeset 3842 b55686a7b22c
parent 2810 c4e16b36bc57
child 4897 be11be0b6ea1
     1.1 --- a/src/HOL/IMP/Hoare.thy	Fri Oct 10 18:37:49 1997 +0200
     1.2 +++ b/src/HOL/IMP/Hoare.thy	Fri Oct 10 19:02:28 1997 +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[a s/x])} 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}"