changeset 556 | 3c214b215f7e |
parent 554 | 638ed040e6f8 |
child 559 | ffa5c4ec9611 |
--- a/ProgTutorial/Tactical.thy Sun Apr 06 12:45:54 2014 +0100 +++ b/ProgTutorial/Tactical.thy Wed May 28 12:41:09 2014 +0100 @@ -388,7 +388,7 @@ lemma shows "False \<Longrightarrow> True" -apply(tactic {* print_tac "foo message" *}) +apply(tactic {* print_tac @{context} "foo message" *}) txt{*gives: \begin{isabelle} @{text "foo message"}\\[3mm]