src/ZF/simpdata.ML
changeset 5137 60205b0de9b9
parent 4091 771b1f6422a8
child 5202 084ceb3844f5
     1.1 --- a/src/ZF/simpdata.ML	Mon Jul 13 16:42:27 1998 +0200
     1.2 +++ b/src/ZF/simpdata.ML	Mon Jul 13 16:43:57 1998 +0200
     1.3 @@ -104,6 +104,7 @@
     1.4  
     1.5  val ZF_atomize = atomize (ZF_conn_pairs, ZF_mem_pairs);
     1.6  
     1.7 -simpset_ref() := simpset() setmksimps (map mk_meta_eq o ZF_atomize o gen_all);
     1.8 +simpset_ref() := simpset() setmksimps (map mk_meta_eq o ZF_atomize o gen_all)
     1.9 +                           addsplits [split_if];
    1.10  
    1.11  val ZF_ss = simpset();