| changeset 45212 | e87feee00a4c |
| parent 43158 | 686fa0a0696e |
| child 47818 | 151d137f1095 |
--- a/src/HOL/IMP/Hoare.thy Wed Oct 19 23:07:48 2011 +0200 +++ b/src/HOL/IMP/Hoare.thy Thu Oct 20 09:48:00 2011 +0200 @@ -8,7 +8,7 @@ type_synonym assn = "state \<Rightarrow> bool" -abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> name \<Rightarrow> state" +abbreviation state_subst :: "state \<Rightarrow> aexp \<Rightarrow> vname \<Rightarrow> state" ("_[_'/_]" [1000,0,0] 999) where "s[a/x] == s(x := aval a s)"