src/ZF/ZF.ML
changeset 12372 cd3a09c7dac9
parent 11770 b6bb7a853dd2
child 12836 5ef96e63fba6
--- a/src/ZF/ZF.ML	Wed Dec 05 03:06:05 2001 +0100
+++ b/src/ZF/ZF.ML	Wed Dec 05 03:07:44 2001 +0100
@@ -45,7 +45,6 @@
 
 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;