| changeset 42053 | 006095137a81 |
| parent 41818 | 6d4c3ee8219d |
| child 42086 | 74bf78db0d87 |
--- a/src/HOL/Isar_Examples/Hoare.thy Tue Mar 22 15:32:47 2011 +0100 +++ b/src/HOL/Isar_Examples/Hoare.thy Tue Mar 22 16:15:50 2011 +0100 @@ -302,7 +302,7 @@ then show ?thesis by simp qed -lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P" +lemma assign: "|- P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P" by (rule basic) text {* Note that above formulation of assignment corresponds to our