fixed typo in comment
Thu, 27 Aug 2015 19:55:43 +0200
changeset 61028 99d58362eeeb
parent 61027 06ceb6dcdccd
child 61029 b09461b3bc05
fixed typo in comment
--- a/src/HOL/IMP/Hoare_Examples.thy	Wed Aug 26 14:59:26 2015 +0200
+++ b/src/HOL/IMP/Hoare_Examples.thy	Thu Aug 27 19:55:43 2015 +0200
@@ -60,12 +60,12 @@
    apply(rule Assign)
   apply(rule Assign')
   apply simp
- apply(simp)
+ apply simp
 apply(rule Assign')
 apply simp
-text{* The proof is intentionally an apply skript because it merely composes
+text{* The proof is intentionally an apply script because it merely composes
 the rules of Hoare logic. Of course, in a few places side conditions have to
 be proved. But since those proofs are 1-liners, a structured proof is
 overkill. In fact, we shall learn later that the application of the Hoare