diff -r 034150db9d91 -r c3dbc04471a9 ProgTutorial/Solutions.thy --- 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\ text \ - 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. \