equal
deleted
inserted
replaced
1 (* Title: Tools/split_rule.ML |
1 (* Title: Tools/split_rule.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen |
3 Author: Stefan Berghofer, David von Oheimb, and Markus Wenzel, TU Muenchen |
4 |
4 |
5 SOME tools for managing tupled arguments and abstractions in rules. |
5 Some tools for managing tupled arguments and abstractions in rules. |
6 *) |
6 *) |
7 |
7 |
8 signature BASIC_SPLIT_RULE = |
8 signature BASIC_SPLIT_RULE = |
9 sig |
9 sig |
10 val split_rule: thm -> thm |
10 val split_rule: thm -> thm |
128 end; |
128 end; |
129 |
129 |
130 |
130 |
131 (* attribute syntax *) |
131 (* attribute syntax *) |
132 |
132 |
|
133 (* FIXME dynamically scoped due to Args.name/pair_tac *) |
|
134 |
133 fun split_format x = Attrib.syntax |
135 fun split_format x = Attrib.syntax |
134 (Scan.lift (Args.parens (Args.$$$ "complete")) |
136 (Scan.lift (Args.parens (Args.$$$ "complete")) |
135 >> K (Drule.rule_attribute (K complete_split_rule)) || |
137 >> K (Drule.rule_attribute (K complete_split_rule)) || |
136 Args.and_list1 (Scan.lift (Scan.repeat Args.name)) |
138 Args.and_list1 (Scan.lift (Scan.repeat Args.name)) |
137 >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x; |
139 >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x; |