src/ZF/simpdata.ML

--- a/src/ZF/simpdata.ML	Thu Sep 07 21:10:11 2000 +0200
+++ b/src/ZF/simpdata.ML	Thu Sep 07 21:12:49 2000 +0200
@@ -63,6 +63,13 @@
 
 end;
 
+bind_thms ("ball_simps", ball_simps);
+bind_thm ("ball_conj_distrib", ball_conj_distrib);
+bind_thms ("bex_simps", bex_simps);
+bind_thm ("bex_disj_distrib", bex_disj_distrib);
+bind_thms ("Rep_simps", Rep_simps);
+bind_thms ("misc_simps", misc_simps);
+
 Addsimps (ball_simps @ bex_simps @ Rep_simps @ misc_simps);