equal
deleted
inserted
replaced
131 fun tag x = Scan.lift (Args.name -- Scan.repeat Args.name) x; |
131 fun tag x = Scan.lift (Args.name -- Scan.repeat Args.name) x; |
132 |
132 |
133 |
133 |
134 (* theorems *) |
134 (* theorems *) |
135 |
135 |
|
136 val thm_sel = Args.parens (Scan.pass () (Args.enum1 "," (Scan.lift |
|
137 ( Args.nat --| Args.$$$ "-" -- Args.nat >> op upto |
|
138 || Args.nat >> single)) >> flat)); |
|
139 |
136 fun gen_thm get attrib app = |
140 fun gen_thm get attrib app = |
137 Scan.depend (fn st => Args.name -- Args.opt_attribs >> |
141 Scan.depend (fn st => Args.name -- Scan.option thm_sel -- Args.opt_attribs >> |
138 (fn (name, srcs) => app ((st, get st name), map (attrib st) srcs))); |
142 (fn (name, srcs) => app ((st, get st name), map (attrib st) srcs))); |
139 |
143 |
140 val global_thm = gen_thm PureThy.get_thm global_attribute Thm.apply_attributes; |
144 val global_thm = gen_thm PureThy.get_thm global_attribute Thm.apply_attributes; |
141 val global_thms = gen_thm PureThy.get_thms global_attribute Thm.applys_attributes; |
145 val global_thms = gen_thm PureThy.get_thms global_attribute Thm.applys_attributes; |
142 val global_thmss = Scan.repeat global_thms >> flat; |
146 val global_thmss = Scan.repeat global_thms >> flat; |