--- a/src/Doc/Sugar/Sugar.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/Doc/Sugar/Sugar.thy Thu Nov 12 13:50:54 2015 +0100
@@ -2,6 +2,8 @@
theory Sugar
imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
begin
+no_translations
+ ("prop") "P \<and> Q \<Longrightarrow> R" <= ("prop") "P \<Longrightarrow> Q \<Longrightarrow> R"
(*>*)
text{*
\section{Introduction}
@@ -115,6 +117,10 @@
\section{Printing theorems}
+The @{prop "P \<Longrightarrow> Q \<Longrightarrow> R"} syntax is a bit idiosyncratic. If you would like
+to avoid it, you can easily print the premises as a conjunction:
+@{prop "P \<and> Q \<Longrightarrow> R"}. See \texttt{OptionalSugar} for the required ``code''.
+
\subsection{Question marks}
If you print anything, especially theorems, containing
--- a/src/HOL/Library/OptionalSugar.thy Thu Nov 12 11:22:26 2015 +0100
+++ b/src/HOL/Library/OptionalSugar.thy Thu Nov 12 13:50:54 2015 +0100
@@ -7,6 +7,10 @@
imports Complex_Main LaTeXsugar
begin
+(* displaying theorems with conjunctions between premises: *)
+translations
+ ("prop") "P \<and> Q \<Longrightarrow> R" <= ("prop") "P \<Longrightarrow> Q \<Longrightarrow> R"
+
(* hiding set *)
translations
"xs" <= "CONST set xs"