--- a/src/ZF/ZF.ML Thu Sep 09 12:25:44 1999 +0200
+++ b/src/ZF/ZF.ML Thu Sep 09 12:26:45 1999 +0200
@@ -46,6 +46,7 @@
AddSIs [ballI];
AddEs [rev_ballE];
+AddXDs [bspec];
(*Takes assumptions ALL x:A.P(x) and a:A; creates assumption P(a)*)
val ball_tac = dtac bspec THEN' assume_tac;