equal
deleted
inserted
replaced
4 *) |
4 *) |
5 (*<*) |
5 (*<*) |
6 theory OptionalSugar |
6 theory OptionalSugar |
7 imports Complex_Main LaTeXsugar |
7 imports Complex_Main LaTeXsugar |
8 begin |
8 begin |
|
9 |
|
10 (* displaying theorems with conjunctions between premises: *) |
|
11 translations |
|
12 ("prop") "P \<and> Q \<Longrightarrow> R" <= ("prop") "P \<Longrightarrow> Q \<Longrightarrow> R" |
9 |
13 |
10 (* hiding set *) |
14 (* hiding set *) |
11 translations |
15 translations |
12 "xs" <= "CONST set xs" |
16 "xs" <= "CONST set xs" |
13 |
17 |