changeset 29493 | ddcbd5e4041d |
parent 27688 | 397de75836a1 |
child 30304 | d8e4cd2ac2a1 |
29492:b19b8793b71c | 29493:ddcbd5e4041d |
---|---|
1 (* Title: HOL/Library/LaTeXsugar.thy |
1 (* Title: HOL/Library/LaTeXsugar.thy |
2 ID: $Id$ |
|
3 Author: Gerwin Klain, Tobias Nipkow, Norbert Schirmer |
2 Author: Gerwin Klain, Tobias Nipkow, Norbert Schirmer |
4 Copyright 2005 NICTA and TUM |
3 Copyright 2005 NICTA and TUM |
5 *) |
4 *) |
6 |
5 |
7 (*<*) |
6 (*<*) |