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"