Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/IMP/Hoare.thy
changeset 4897 be11be0b6ea1
parent 3842 b55686a7b22c
child 5102 8c782c25a11e 
--- a/src/HOL/IMP/Hoare.thy	Tue May 05 17:28:22 1998 +0200
+++ b/src/HOL/IMP/Hoare.thy	Wed May 06 11:46:00 1998 +0200
@@ -20,7 +20,7 @@
 inductive hoare
 intrs
   skip "|- {P}SKIP{P}"
-  ass  "|- {%s. P(s[a s/x])} x:=a {P}"
+  ass  "|- {%s. P(s[x:=a s])} x:=a {P}"
   semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}"
   If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==>
       |- {P} IF b THEN c ELSE d {Q}"
isabelle