# 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);