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>