src/ZF/simpdata.ML
changeset 35762 af3ff2ba4c54
parent 35409 5c5bb83f2bae
child 36543 0e7fc5bf38de
--- a/src/ZF/simpdata.ML	Sat Mar 13 16:37:15 2010 +0100
+++ b/src/ZF/simpdata.ML	Sat Mar 13 16:44:12 2010 +0100
@@ -1,9 +1,8 @@
-(*  Title:      ZF/simpdata
-    ID:         $Id$
+(*  Title:      ZF/simpdata.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1991  University of Cambridge
 
-Rewriting for ZF set theory: specialized extraction of rewrites from theorems
+Rewriting for ZF set theory: specialized extraction of rewrites from theorems.
 *)
 
 (*** New version of mk_rew_rules ***)