src/Tools/IsaPlanner/rw_inst.ML
changeset 23175 267ba70e7a9d
parent 23171 861f63a35d31
child 29265 5b4247055bd7
     1.1 --- a/src/Tools/IsaPlanner/rw_inst.ML	Thu May 31 20:55:33 2007 +0200
     1.2 +++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu May 31 21:09:14 2007 +0200
     1.3 @@ -1,18 +1,11 @@
     1.4 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
     1.5 -(*  Title:      Pure/IsaPlanner/rw_inst.ML
     1.6 +(*  Title:      Tools/IsaPlanner/rw_inst.ML
     1.7      ID:         $Id$
     1.8      Author:     Lucas Dixon, University of Edinburgh
     1.9 -                lucas.dixon@ed.ac.uk
    1.10 -    Created:    25 Aug 2004
    1.11 -*)
    1.12 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
    1.13 -(*  DESCRIPTION:
    1.14  
    1.15 -    rewriting using a conditional meta-equality theorem which supports 
    1.16 -    schematic variable instantiation.
    1.17 +Rewriting using a conditional meta-equality theorem which supports
    1.18 +schematic variable instantiation.
    1.19 +*)   
    1.20  
    1.21 -*)   
    1.22 -(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
    1.23  signature RW_INST =
    1.24  sig
    1.25