header;
authorwenzelm
Thu Jun 02 09:11:32 2005 +0200 (2005-06-02)
changeset 16179fa7e70be26b0
parent 16178 754efc5afd5d
child 16180 a51be5cbd81d
header;
src/HOL/eqrule_HOL_data.ML
src/Pure/General/susp.ML
src/Pure/IsaPlanner/focus_term_lib.ML
src/Pure/IsaPlanner/isa_fterm.ML
src/Pure/IsaPlanner/isand.ML
src/Pure/IsaPlanner/isaplib.ML
src/Pure/IsaPlanner/rw_inst.ML
src/Pure/IsaPlanner/rw_tools.ML
src/Pure/IsaPlanner/term_lib.ML
src/Pure/IsaPlanner/upterm_lib.ML
src/Pure/search.ML
src/Pure/tctical.ML
     1.1 --- a/src/HOL/eqrule_HOL_data.ML	Thu Jun 02 02:21:44 2005 +0200
     1.2 +++ b/src/HOL/eqrule_HOL_data.ML	Thu Jun 02 09:11:32 2005 +0200
     1.3 @@ -1,5 +1,6 @@
     1.4  (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     1.5 -(*  Title:      sys/eqrule_HOL_data.ML
     1.6 +(*  Title:      HOL/eqrule_HOL_data.ML
     1.7 +    Id:		$Id$
     1.8      Author:     Lucas Dixon, University of Edinburgh
     1.9                  lucas.dixon@ed.ac.uk
    1.10      Modified:   22 July 2004
     2.1 --- a/src/Pure/General/susp.ML	Thu Jun 02 02:21:44 2005 +0200
     2.2 +++ b/src/Pure/General/susp.ML	Thu Jun 02 09:11:32 2005 +0200
     2.3 @@ -1,3 +1,10 @@
     2.4 +(*  Title:      Pure/General/susp.ML
     2.5 +    ID:         $Id$
     2.6 +    Author:     Sebastian Skalberg, TU Muenchen
     2.7 +
     2.8 +Delayed evaluation.
     2.9 +*)
    2.10 +
    2.11  signature SUSP =
    2.12  sig
    2.13  
     3.1 --- a/src/Pure/IsaPlanner/focus_term_lib.ML	Thu Jun 02 02:21:44 2005 +0200
     3.2 +++ b/src/Pure/IsaPlanner/focus_term_lib.ML	Thu Jun 02 09:11:32 2005 +0200
     3.3 @@ -1,5 +1,6 @@
     3.4  (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     3.5 -(*  Title:      libs/focus_term_lib.ML
     3.6 +(*  Title:      Pure/IsaPlanner/focus_term_lib.ML
     3.7 +    ID:		$Id$
     3.8      Author:     Lucas Dixon, University of Edinburgh
     3.9                  lucasd@dai.ed.ac.uk
    3.10      Date:       16 April 2003
     4.1 --- a/src/Pure/IsaPlanner/isa_fterm.ML	Thu Jun 02 02:21:44 2005 +0200
     4.2 +++ b/src/Pure/IsaPlanner/isa_fterm.ML	Thu Jun 02 09:11:32 2005 +0200
     4.3 @@ -1,5 +1,6 @@
     4.4  (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     4.5 -(*  Title:      libs/isa_fterm.ML
     4.6 +(*  Title:      Pure/IsaPlanner/isa_fterm.ML
     4.7 +    ID:		$Id$
     4.8      Author:     Lucas Dixon, University of Edinburgh
     4.9                  lucasd@dai.ed.ac.uk
    4.10      Date:       16 April 2003
     5.1 --- a/src/Pure/IsaPlanner/isand.ML	Thu Jun 02 02:21:44 2005 +0200
     5.2 +++ b/src/Pure/IsaPlanner/isand.ML	Thu Jun 02 09:11:32 2005 +0200
     5.3 @@ -1,5 +1,6 @@
     5.4  (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     5.5 -(*  Title:      isand.ML
     5.6 +(*  Title:      Pure/IsaPlanner/isand.ML
     5.7 +    ID:		$Id$
     5.8      Author:     Lucas Dixon, University of Edinburgh
     5.9                  lucas.dixon@ed.ac.uk
    5.10      Updated:    26 Apr 2005
     6.1 --- a/src/Pure/IsaPlanner/isaplib.ML	Thu Jun 02 02:21:44 2005 +0200
     6.2 +++ b/src/Pure/IsaPlanner/isaplib.ML	Thu Jun 02 09:11:32 2005 +0200
     6.3 @@ -1,5 +1,6 @@
     6.4  (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     6.5 -(*  Title:      generic/isaplib.ML
     6.6 +(*  Title:      Pure/IsaPlanner/isaplib.ML
     6.7 +    ID:		$Id$
     6.8      Author:     Lucas Dixon, University of Edinburgh
     6.9                  lucasd@dai.ed.ac.uk
    6.10  *)
     7.1 --- a/src/Pure/IsaPlanner/rw_inst.ML	Thu Jun 02 02:21:44 2005 +0200
     7.2 +++ b/src/Pure/IsaPlanner/rw_inst.ML	Thu Jun 02 09:11:32 2005 +0200
     7.3 @@ -1,5 +1,6 @@
     7.4  (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     7.5 -(*  Title:      sys/rw_inst.ML
     7.6 +(*  Title:      Pure/IsaPlanner/rw_inst.ML
     7.7 +    ID:         $Id$
     7.8      Author:     Lucas Dixon, University of Edinburgh
     7.9                  lucas.dixon@ed.ac.uk
    7.10      Created:    25 Aug 2004
     8.1 --- a/src/Pure/IsaPlanner/rw_tools.ML	Thu Jun 02 02:21:44 2005 +0200
     8.2 +++ b/src/Pure/IsaPlanner/rw_tools.ML	Thu Jun 02 09:11:32 2005 +0200
     8.3 @@ -1,5 +1,6 @@
     8.4  (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     8.5 -(*  Title:      sys/rw_tools.ML
     8.6 +(*  Title:      Pure/IsaPlanner/rw_tools.ML
     8.7 +    ID:		$Id$
     8.8      Author:     Lucas Dixon, University of Edinburgh
     8.9                  lucas.dixon@ed.ac.uk
    8.10      Created:    28 May 2004
     9.1 --- a/src/Pure/IsaPlanner/term_lib.ML	Thu Jun 02 02:21:44 2005 +0200
     9.2 +++ b/src/Pure/IsaPlanner/term_lib.ML	Thu Jun 02 09:11:32 2005 +0200
     9.3 @@ -1,5 +1,6 @@
     9.4  (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     9.5 -(*  Title:      libs/term_lib.ML
     9.6 +(*  Title:      Pure/IsaPlanner/term_lib.ML
     9.7 +    ID:		$Id$
     9.8      Author:     Lucas Dixon, University of Edinburgh
     9.9                  lucasd@dai.ed.ac.uk
    9.10      Created:    17 Aug 2002
    10.1 --- a/src/Pure/IsaPlanner/upterm_lib.ML	Thu Jun 02 02:21:44 2005 +0200
    10.2 +++ b/src/Pure/IsaPlanner/upterm_lib.ML	Thu Jun 02 09:11:32 2005 +0200
    10.3 @@ -1,5 +1,6 @@
    10.4  (* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    10.5 -(*  Title:      libs/upterm_lib.ML
    10.6 +(*  Title:      Pure/IsaPlanner/upterm_lib.ML
    10.7 +    ID:		$Id$
    10.8      Author:     Lucas Dixon, University of Edinburgh
    10.9                  lucas.dixon@ed.ac.uk
   10.10      Created:    26 Jan 2004
    11.1 --- a/src/Pure/search.ML	Thu Jun 02 02:21:44 2005 +0200
    11.2 +++ b/src/Pure/search.ML	Thu Jun 02 09:11:32 2005 +0200
    11.3 @@ -1,8 +1,8 @@
    11.4 -(*  Title: 	search
    11.5 +(*  Title: 	Pure/search.ML
    11.6      ID:         $Id$
    11.7      Author: 	Lawrence C Paulson and Norbert Voelker
    11.8  
    11.9 -Search tacticals
   11.10 +Search tacticals.
   11.11  *)
   11.12  
   11.13  infix 1 THEN_MAYBE THEN_MAYBE';
    12.1 --- a/src/Pure/tctical.ML	Thu Jun 02 02:21:44 2005 +0200
    12.2 +++ b/src/Pure/tctical.ML	Thu Jun 02 09:11:32 2005 +0200
    12.3 @@ -1,9 +1,9 @@
    12.4 -(*  Title:      tctical
    12.5 +(*  Title:      Pure/tctical.ML
    12.6      ID:         $Id$
    12.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    12.8      Copyright   1993  University of Cambridge
    12.9  
   12.10 -Tacticals
   12.11 +Tacticals.
   12.12  *)
   12.13  
   12.14  infix 1 THEN THEN' THEN_ALL_NEW;