src/HOL/Library/LaTeXsugar.thy
changeset 29493 ddcbd5e4041d
parent 27688 397de75836a1
child 30304 d8e4cd2ac2a1
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Thu Jan 15 14:52:23 2009 +0100
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Thu Jan 15 14:52:24 2009 +0100
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Library/LaTeXsugar.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Gerwin Klain, Tobias Nipkow, Norbert Schirmer
     1.7      Copyright   2005 NICTA and TUM
     1.8  *)