equal
deleted
inserted
replaced
126 |
126 |
127 |
127 |
128 (* attribute syntax *) |
128 (* attribute syntax *) |
129 |
129 |
130 fun split_format x = Attrib.syntax |
130 fun split_format x = Attrib.syntax |
131 (Args.mode "complete" >> K (Drule.rule_attribute (K complete_split_rule)) || |
131 (Scan.lift (Args.parens (Args.$$$ "complete")) |
132 Args.and_list1 (Scan.lift (Scan.repeat Args.name)) |
132 >> K (Drule.rule_attribute (K complete_split_rule)) || |
133 >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x; |
133 Args.and_list1 (Scan.lift (Scan.repeat Args.name)) |
|
134 >> (fn xss => Drule.rule_attribute (K (split_rule_goal xss)))) x; |
134 |
135 |
135 val setup = |
136 val setup = |
136 [Attrib.add_attributes |
137 [Attrib.add_attributes |
137 [("split_format", (split_format, split_format), |
138 [("split_format", (split_format, split_format), |
138 "split pair-typed subterms in premises, or function arguments")]]; |
139 "split pair-typed subterms in premises, or function arguments")]]; |