changeset 55052 | c602013f127e |
parent 55038 | f2179be64805 |
child 56245 | 84fc7dfa3cd4 |
--- a/src/HOL/Library/OptionalSugar.thy Mon Jan 20 10:07:07 2014 +0100 +++ b/src/HOL/Library/OptionalSugar.thy Mon Jan 20 12:20:23 2014 +0100 @@ -1,5 +1,5 @@ (* Title: HOL/Library/OptionalSugar.thy - Author: Gerwin Klain, Tobias Nipkow + Author: Gerwin Klein, Tobias Nipkow Copyright 2005 NICTA and TUM *) (*<*)