equal
deleted
inserted
replaced
144 |
144 |
145 (* attribute syntax *) |
145 (* attribute syntax *) |
146 |
146 |
147 (* FIXME dynamically scoped due to Args.name/pair_tac *) |
147 (* FIXME dynamically scoped due to Args.name/pair_tac *) |
148 |
148 |
149 val split_format = Attrib.syntax |
149 val split_format = Attrib.syntax (Scan.lift |
150 (Scan.lift (Args.parens (Args.$$$ "complete")) |
150 (Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) || |
151 >> K (Thm.rule_attribute (K complete_split_rule)) || |
151 OuterParse.and_list1 (Scan.repeat Args.name) |
152 Args.and_list1 (Scan.lift (Scan.repeat Args.name)) |
|
153 >> (fn xss => Thm.rule_attribute (fn context => |
152 >> (fn xss => Thm.rule_attribute (fn context => |
154 split_rule_goal (Context.proof_of context) xss))); |
153 split_rule_goal (Context.proof_of context) xss)))); |
155 |
154 |
156 val setup = |
155 val setup = |
157 Attrib.add_attributes |
156 Attrib.add_attributes |
158 [("split_format", split_format, |
157 [("split_format", split_format, |
159 "split pair-typed subterms in premises, or function arguments"), |
158 "split pair-typed subterms in premises, or function arguments"), |