src/Tools/IsaPlanner/zipper.ML
changeset 23175 267ba70e7a9d
parent 23171 861f63a35d31
child 30161 c26e515f1c29
     1.1 --- a/src/Tools/IsaPlanner/zipper.ML	Thu May 31 20:55:33 2007 +0200
     1.2 +++ b/src/Tools/IsaPlanner/zipper.ML	Thu May 31 21:09:14 2007 +0200
     1.3 @@ -1,17 +1,10 @@
     1.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     1.5 -(*  Title:      Pure/IsaPlanner/zipper.ML
     1.6 +(*  Title:      Tools/IsaPlanner/zipper.ML
     1.7      ID:		$Id$
     1.8      Author:     Lucas Dixon, University of Edinburgh
     1.9 -                lucas.dixon@ed.ac.uk
    1.10 -    Created:    24 Mar 2006
    1.11 -*)
    1.12 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    1.13 -(*  DESCRIPTION:
    1.14 -    A notion roughly based on Huet's Zippers for Isabelle terms.
    1.15 +
    1.16 +A notion roughly based on Huet's Zippers for Isabelle terms.
    1.17  *)   
    1.18  
    1.19 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    1.20 -
    1.21  (* abstract term for no more than pattern matching *)
    1.22  signature ABSTRACT_TRM = 
    1.23  sig