changeset 55077 | 4cf280104b85 |
parent 49628 | 8262d35eff20 |
child 55114 | 0ee5c17f2207 |
55076:1e73e090a514 | 55077:4cf280104b85 |
---|---|
1 (* Title: HOL/Library/LaTeXsugar.thy |
1 (* Title: HOL/Library/LaTeXsugar.thy |
2 Author: Gerwin Klain, Tobias Nipkow, Norbert Schirmer |
2 Author: Gerwin Klein, Tobias Nipkow, Norbert Schirmer |
3 Copyright 2005 NICTA and TUM |
3 Copyright 2005 NICTA and TUM |
4 *) |
4 *) |
5 |
5 |
6 (*<*) |
6 (*<*) |
7 theory LaTeXsugar |
7 theory LaTeXsugar |