--- a/src/Pure/search.ML Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/search.ML Thu Jun 02 09:11:32 2005 +0200
@@ -1,8 +1,8 @@
-(* Title: search
+(* Title: Pure/search.ML
ID: $Id$
Author: Lawrence C Paulson and Norbert Voelker
-Search tacticals
+Search tacticals.
*)
infix 1 THEN_MAYBE THEN_MAYBE';