equal
deleted
inserted
replaced
301 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]"); |
301 val attribs = $$$ "[" |-- !!! (list attrib --| $$$ "]"); |
302 val opt_attribs = Scan.optional attribs []; |
302 val opt_attribs = Scan.optional attribs []; |
303 |
303 |
304 fun thm_name s = name -- opt_attribs --| $$$ s; |
304 fun thm_name s = name -- opt_attribs --| $$$ s; |
305 fun opt_thm_name s = |
305 fun opt_thm_name s = |
306 Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []);; |
306 Scan.optional ((name -- opt_attribs || (attribs >> pair "")) --| $$$ s) ("", []); |
307 |
307 |
308 val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y)); |
308 val spec_name = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y)); |
309 val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y)); |
309 val spec_opt_name = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y)); |
310 |
310 |
311 val thm_sel = $$$ "(" |-- list1 |
311 val thm_sel = $$$ "(" |-- list1 |