# HG changeset patch
# User wenzelm
# Date 1117696292 -7200
# Node ID fa7e70be26b0a84abc4cf7c2cfd00badbdd32ff7
# Parent  754efc5afd5d2196ffac50e2cf58aee2532665ea
header;

diff -r 754efc5afd5d -r fa7e70be26b0 src/HOL/eqrule_HOL_data.ML
--- a/src/HOL/eqrule_HOL_data.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/HOL/eqrule_HOL_data.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,5 +1,6 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      sys/eqrule_HOL_data.ML
+(*  Title:      HOL/eqrule_HOL_data.ML
+    Id:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucas.dixon@ed.ac.uk
     Modified:   22 July 2004
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/General/susp.ML
--- a/src/Pure/General/susp.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/General/susp.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,3 +1,10 @@
+(*  Title:      Pure/General/susp.ML
+    ID:         $Id$
+    Author:     Sebastian Skalberg, TU Muenchen
+
+Delayed evaluation.
+*)
+
 signature SUSP =
 sig
 
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/IsaPlanner/focus_term_lib.ML
--- a/src/Pure/IsaPlanner/focus_term_lib.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/IsaPlanner/focus_term_lib.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,5 +1,6 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      libs/focus_term_lib.ML
+(*  Title:      Pure/IsaPlanner/focus_term_lib.ML
+    ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucasd@dai.ed.ac.uk
     Date:       16 April 2003
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/IsaPlanner/isa_fterm.ML
--- a/src/Pure/IsaPlanner/isa_fterm.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/IsaPlanner/isa_fterm.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,5 +1,6 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      libs/isa_fterm.ML
+(*  Title:      Pure/IsaPlanner/isa_fterm.ML
+    ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucasd@dai.ed.ac.uk
     Date:       16 April 2003
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/IsaPlanner/isand.ML
--- a/src/Pure/IsaPlanner/isand.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/IsaPlanner/isand.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,5 +1,6 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      isand.ML
+(*  Title:      Pure/IsaPlanner/isand.ML
+    ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucas.dixon@ed.ac.uk
     Updated:    26 Apr 2005
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/IsaPlanner/isaplib.ML
--- a/src/Pure/IsaPlanner/isaplib.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/IsaPlanner/isaplib.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,5 +1,6 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      generic/isaplib.ML
+(*  Title:      Pure/IsaPlanner/isaplib.ML
+    ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucasd@dai.ed.ac.uk
 *)
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/IsaPlanner/rw_inst.ML
--- a/src/Pure/IsaPlanner/rw_inst.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/IsaPlanner/rw_inst.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,5 +1,6 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      sys/rw_inst.ML
+(*  Title:      Pure/IsaPlanner/rw_inst.ML
+    ID:         $Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucas.dixon@ed.ac.uk
     Created:    25 Aug 2004
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/IsaPlanner/rw_tools.ML
--- a/src/Pure/IsaPlanner/rw_tools.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/IsaPlanner/rw_tools.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,5 +1,6 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      sys/rw_tools.ML
+(*  Title:      Pure/IsaPlanner/rw_tools.ML
+    ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucas.dixon@ed.ac.uk
     Created:    28 May 2004
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/IsaPlanner/term_lib.ML
--- a/src/Pure/IsaPlanner/term_lib.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/IsaPlanner/term_lib.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,5 +1,6 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      libs/term_lib.ML
+(*  Title:      Pure/IsaPlanner/term_lib.ML
+    ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucasd@dai.ed.ac.uk
     Created:    17 Aug 2002
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/IsaPlanner/upterm_lib.ML
--- a/src/Pure/IsaPlanner/upterm_lib.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/IsaPlanner/upterm_lib.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,5 +1,6 @@
 (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      libs/upterm_lib.ML
+(*  Title:      Pure/IsaPlanner/upterm_lib.ML
+    ID:		$Id$
     Author:     Lucas Dixon, University of Edinburgh
                 lucas.dixon@ed.ac.uk
     Created:    26 Jan 2004
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/search.ML
--- 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';
diff -r 754efc5afd5d -r fa7e70be26b0 src/Pure/tctical.ML
--- a/src/Pure/tctical.ML	Thu Jun 02 02:21:44 2005 +0200
+++ b/src/Pure/tctical.ML	Thu Jun 02 09:11:32 2005 +0200
@@ -1,9 +1,9 @@
-(*  Title:      tctical
+(*  Title:      Pure/tctical.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-Tacticals
+Tacticals.
 *)
 
 infix 1 THEN THEN' THEN_ALL_NEW;