| changeset 8154 | dab09e1ad594 |
| parent 8100 | 6186ee807f2e |
| child 8168 | 9d2ac5439089 |
| 8153:9bdbcb71dc56 | 8154:dab09e1ad594 |
|---|---|
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 (FIRSTGOAL record_split_tac)), |
523 ("record_split", Method.no_args (Method.METHOD0 (FINDGOAL 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 **) |