# HG changeset patch
# User nipkow
# Date 1413209231 -7200
# Node ID 46a19b1d3dd230dae5e1193cd6e45f8c43847ca8
# Parent  3e1cad27fc2f4e119be433c1448ad4e7f3dcee05
tuned

diff -r 3e1cad27fc2f -r 46a19b1d3dd2 src/Doc/Prog_Prove/Basics.thy
--- a/src/Doc/Prog_Prove/Basics.thy	Sun Oct 12 21:52:45 2014 +0200
+++ b/src/Doc/Prog_Prove/Basics.thy	Mon Oct 13 16:07:11 2014 +0200
@@ -86,7 +86,8 @@
 Right-arrows of all kinds always associate to the right. In particular,
 the formula
 @{text"A\<^sub>1 \<Longrightarrow> A\<^sub>2 \<Longrightarrow> A\<^sub>3"} means @{text "A\<^sub>1 \<Longrightarrow> (A\<^sub>2 \<Longrightarrow> A\<^sub>3)"}.
-The (Isabelle-specific) notation \mbox{@{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}}
+The (Isabelle-specific\footnote{To display implications in this style in
+Isabelle/jedit you need to set Plugins $>$ Plugin Options $>$ Isabelle/General $>$ Print Mode to ``\texttt{brackets}'' and restart.}) notation \mbox{@{text"\<lbrakk> A\<^sub>1; \<dots>; A\<^sub>n \<rbrakk> \<Longrightarrow> A"}}
 is short for the iterated implication \mbox{@{text"A\<^sub>1 \<Longrightarrow> \<dots> \<Longrightarrow> A\<^sub>n \<Longrightarrow> A"}}.
 Sometimes we also employ inference rule notation:
 \inferrule{\mbox{@{text "A\<^sub>1"}}\\ \mbox{@{text "\<dots>"}}\\ \mbox{@{text "A\<^sub>n"}}}