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