# HG changeset patch # User blanchet # Date 1390238744 -3600 # Node ID 4cf280104b85455676944e5c91e48df99901b01e # Parent 1e73e090a514df8e6a2c597ebf841e16e291853b fixed typo diff -r 1e73e090a514 -r 4cf280104b85 src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy Mon Jan 20 18:24:56 2014 +0100 +++ b/src/HOL/Library/LaTeXsugar.thy Mon Jan 20 18:25:44 2014 +0100 @@ -1,5 +1,5 @@ (* Title: HOL/Library/LaTeXsugar.thy - Author: Gerwin Klain, Tobias Nipkow, Norbert Schirmer + Author: Gerwin Klein, Tobias Nipkow, Norbert Schirmer Copyright 2005 NICTA and TUM *) @@ -114,4 +114,4 @@ *} end -(*>*) \ No newline at end of file +(*>*)