src/Tools/IsaPlanner/rw_inst.ML
changeset 23175 267ba70e7a9d
parent 23171 861f63a35d31
child 29265 5b4247055bd7
--- a/src/Tools/IsaPlanner/rw_inst.ML	Thu May 31 20:55:33 2007 +0200
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Thu May 31 21:09:14 2007 +0200
@@ -1,18 +1,11 @@
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  Title:      Pure/IsaPlanner/rw_inst.ML
+(*  Title:      Tools/IsaPlanner/rw_inst.ML
     ID:         $Id$
     Author:     Lucas Dixon, University of Edinburgh
-                lucas.dixon@ed.ac.uk
-    Created:    25 Aug 2004
-*)
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *) 
-(*  DESCRIPTION:
 
-    rewriting using a conditional meta-equality theorem which supports 
-    schematic variable instantiation.
+Rewriting using a conditional meta-equality theorem which supports
+schematic variable instantiation.
+*)   
 
-*)   
-(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=- *)
 signature RW_INST =
 sig