equal
deleted
inserted
replaced
386 as the user would see it. For example, processing the proof |
386 as the user would see it. For example, processing the proof |
387 *} |
387 *} |
388 |
388 |
389 lemma |
389 lemma |
390 shows "False \<Longrightarrow> True" |
390 shows "False \<Longrightarrow> True" |
391 apply(tactic {* print_tac "foo message" *}) |
391 apply(tactic {* print_tac @{context} "foo message" *}) |
392 txt{*gives: |
392 txt{*gives: |
393 \begin{isabelle} |
393 \begin{isabelle} |
394 @{text "foo message"}\\[3mm] |
394 @{text "foo message"}\\[3mm] |
395 @{prop "False \<Longrightarrow> True"}\\ |
395 @{prop "False \<Longrightarrow> True"}\\ |
396 @{text " 1. False \<Longrightarrow> True"}\\ |
396 @{text " 1. False \<Longrightarrow> True"}\\ |