changeset 5553 | ae42b36a50c2 |
parent 5325 | f7a5e06adea1 |
child 6153 | bff90585cce5 |
--- a/src/ZF/simpdata.ML Thu Sep 24 17:16:06 1998 +0200 +++ b/src/ZF/simpdata.ML Thu Sep 24 17:17:14 1998 +0200 @@ -105,7 +105,7 @@ val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs); -simpset_ref() := simpset() setmksimps (map mk_meta_eq o ZF_atomize o gen_all) +simpset_ref() := simpset() setmksimps (map mk_eq o ZF_atomize o gen_all) addsplits [split_if]; val ZF_ss = simpset();