# HG changeset patch
# User nipkow
# Date 1447332654 -3600
# Node ID ae5e55d03e455c344801ac42030a98dbe54d9c28
# Parent  b1c24adc15814973c1c05ef16a629bc088b7fe5f
translation for conjunctive premises

diff -r b1c24adc1581 -r ae5e55d03e45 src/Doc/Sugar/Sugar.thy
--- 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
diff -r b1c24adc1581 -r ae5e55d03e45 src/HOL/Library/OptionalSugar.thy
--- 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"