equal
deleted
inserted
replaced
203 |
203 |
204 |
204 |
205 (* concrete syntax *) |
205 (* concrete syntax *) |
206 |
206 |
207 fun add_args a b c = Attrib.syntax |
207 fun add_args a b c = Attrib.syntax |
208 (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- Scan.option Args.nat) |
208 (Scan.lift ((Args.bang >> K a || Args.query >> K c || Scan.succeed b) -- |
209 >> (fn (f, n) => f n)); |
209 Scan.option OuterParse.nat) >> (fn (f, n) => f n)); |
210 |
210 |
211 val rule_atts = |
211 val rule_atts = |
212 [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"), |
212 [("intro", add_args intro_bang intro intro_query, "declaration of introduction rule"), |
213 ("elim", add_args elim_bang elim elim_query, "declaration of elimination rule"), |
213 ("elim", add_args elim_bang elim elim_query, "declaration of elimination rule"), |
214 ("dest", add_args dest_bang dest dest_query, "declaration of destruction rule"), |
214 ("dest", add_args dest_bang dest dest_query, "declaration of destruction rule"), |