ProgTutorial/Solutions.thy
changeset 575 c3dbc04471a9
parent 574 034150db9d91
--- a/ProgTutorial/Solutions.thy	Wed May 22 12:38:51 2019 +0200
+++ b/ProgTutorial/Solutions.thy	Wed May 22 13:24:30 2019 +0200
@@ -194,7 +194,7 @@
 end\<close>
 
 text \<open>
-  In Line 11 we apply the rule @{thm [source] impE1} in concjunction 
+  In Line 9 we apply the rule @{thm [source] impE1} in concjunction 
   with @{ML assume_tac} in order to reduce the number of possibilities that
   need to be explored. You can use the tactic as follows.
 \<close>