| changeset 30663 | 0b6aff7451b2 |
| parent 30503 | 201887dcea0a |
| child 32891 | d403b99287ff |
| 30662:396be15b95d5 | 30663:0b6aff7451b2 |
|---|---|
2 Author: Gerwin Klain, Tobias Nipkow |
2 Author: Gerwin Klain, Tobias Nipkow |
3 Copyright 2005 NICTA and TUM |
3 Copyright 2005 NICTA and TUM |
4 *) |
4 *) |
5 (*<*) |
5 (*<*) |
6 theory OptionalSugar |
6 theory OptionalSugar |
7 imports LaTeXsugar Complex_Main |
7 imports Complex_Main LaTeXsugar |
8 begin |
8 begin |
9 |
9 |
10 (* hiding set *) |
10 (* hiding set *) |
11 translations |
11 translations |
12 "xs" <= "CONST set xs" |
12 "xs" <= "CONST set xs" |