| changeset 6092 | d9db67970c73 |
| parent 5888 | d8e51792ca85 |
| child 6214 | 0513cfd1a598 |
| 6091:e3cdbd929a24 | 6092:d9db67970c73 |
|---|---|
420 |
420 |
421 (* attributes *) |
421 (* attributes *) |
422 |
422 |
423 local |
423 local |
424 |
424 |
425 fun gen_rulify x = Attrib.no_args (Attribute.rule (K (normalize_thm [RSspec, RSmp]))) x; |
425 fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x; |
426 |
426 |
427 in |
427 in |
428 |
428 |
429 val attrib_setup = |
429 val attrib_setup = |
430 [Attrib.add_attributes |
430 [Attrib.add_attributes |