# HG changeset patch # User haftmann # Date 1234941791 -3600 # Node ID c7849326100ed0852e0fa6bbd8ad30bd59362b97 # Parent 7a2eb84343f941404c2651f171459ce0e8ea7699 stripped ID diff -r 7a2eb84343f9 -r c7849326100e src/HOL/Induct/Common_Patterns.thy --- a/src/HOL/Induct/Common_Patterns.thy Tue Feb 17 21:51:52 2009 +0100 +++ b/src/HOL/Induct/Common_Patterns.thy Wed Feb 18 08:23:11 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Induct/Common_Patterns.thy - ID: $Id$ Author: Makarius *) diff -r 7a2eb84343f9 -r c7849326100e src/HOL/Library/Enum.thy --- a/src/HOL/Library/Enum.thy Tue Feb 17 21:51:52 2009 +0100 +++ b/src/HOL/Library/Enum.thy Wed Feb 18 08:23:11 2009 +0100 @@ -1,5 +1,4 @@ (* Title: HOL/Library/Enum.thy - ID: $Id$ Author: Florian Haftmann, TU Muenchen *)