author nipkow Mon, 13 Oct 2014 16:07:11 +0200 changeset 58655 46a19b1d3dd2 parent 58654 3e1cad27fc2f child 58656 7f14d5d9b933
tuned
```--- 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"}}}```