| changeset 56073 | 29e308b56d23 |
| parent 55656 | eb07b0acbebc |
| child 58614 | 7338eb25226c |
--- a/src/HOL/Isar_Examples/Hoare_Ex.thy Wed Mar 12 22:57:50 2014 +0100 +++ b/src/HOL/Isar_Examples/Hoare_Ex.thy Thu Mar 13 07:07:07 2014 +0100 @@ -59,7 +59,7 @@ by hoare lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>M := a; \<acute>N := b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>" - by hoare simp + by hoare lemma "\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>