# HG changeset patch
# User wenzelm
# Date 936872805 -7200
# Node ID 99c7e60d6b3fce465bc7581da11d7e9151595fff
# Parent  505f6f8e9dcf2e3bf0c640c9d66a0320021425d1
AddXDs [bspec];

diff -r 505f6f8e9dcf -r 99c7e60d6b3f src/ZF/ZF.ML
--- 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;