| author | wenzelm |
| Thu, 02 Sep 1999 15:24:31 +0200 | |
| changeset 7441 | 20b3e2d2fcb6 |
| parent 7440 | c1829208180f |
| child 7442 | 2d2849258e3f |
| src/HOL/Set.ML | file | annotate | diff | comparison | revisions |
--- 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);