# HG changeset patch
# User wenzelm
# Date 936278671 -7200
# Node ID 20b3e2d2fcb6b211aa54b644222f101c89f7e849
# Parent  c1829208180f9dd94115406c123e9dec7d9f6bcc
AddXDs [bspec];

diff -r c1829208180f -r 20b3e2d2fcb6 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Thu Sep 02 15:24:00 1999 +0200
+++ b/src/HOL/Set.ML	Thu Sep 02 15:24:31 1999 +0200
@@ -57,6 +57,7 @@
 
 AddSIs [ballI];
 AddEs  [ballE];
+AddXDs [bspec];
 (* gives better instantiation for bound: *)
 claset_ref() := claset() addWrapper ("bspec", fn tac2 =>
 			 (dtac bspec THEN' atac) APPEND' tac2);