| changeset 61645 | ae5e55d03e45 |
| parent 61143 | 5f898411ce87 |
| child 61955 | e96292f32c3c |
--- 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"