--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
*)
--- 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
--- 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
--- 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
--- 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
--- 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';
--- 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;