--- a/src/HOL/FunDef.thy Wed Jan 21 16:47:04 2009 +0100 +++ b/src/HOL/FunDef.thy Wed Jan 21 16:47:31 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/FunDef.thy - ID: $Id$ Author: Alexander Krauss, TU Muenchen *)