changeset 7441 | 20b3e2d2fcb6 |
parent 7031 | 972b5f62f476 |
child 7496 | 93ae11d887ff |
--- 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);