# HG changeset patch
# User blanchet
# Date 1440698143 -7200
# Node ID 99d58362eeeb0eca7f34e85f41962a7c939d299e
# Parent  06ceb6dcdccd49f21c83e5922709f47cefedeb5e
fixed typo in comment

diff -r 06ceb6dcdccd -r 99d58362eeeb src/HOL/IMP/Hoare_Examples.thy
--- 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
 done
 
-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