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 ***)