changeset 8168 | 9d2ac5439089 |
parent 8154 | dab09e1ad594 |
child 8246 | efb3c8253d90 |
8167:7574835ed01e | 8168:9d2ac5439089 |
---|---|
518 |
518 |
519 |
519 |
520 (* method *) |
520 (* method *) |
521 |
521 |
522 val record_split_method = |
522 val record_split_method = |
523 ("record_split", Method.no_args (Method.METHOD0 (FINDGOAL record_split_tac)), |
523 ("record_split", Method.no_args (Method.METHOD0 (HEADGOAL record_split_tac)), |
524 "split record fields"); |
524 "split record fields"); |
525 |
525 |
526 |
526 |
527 |
527 |
528 (** internal theory extenders **) |
528 (** internal theory extenders **) |