equal
deleted
inserted
replaced
58 Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat)) |
58 Scan.optional (Parse.$$$ "if" |-- Parse.!!! (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat)) |
59 []; |
59 []; |
60 |
60 |
61 val multi_specs = |
61 val multi_specs = |
62 Parse.enum1 "|" |
62 Parse.enum1 "|" |
63 (opt_thm_name ":" -- Parse.prop -- if_assumes --| |
63 ((opt_thm_name ":" -- Parse.prop -- if_assumes -- Parse.for_fixes >> Scan.triple1) --| |
64 Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|"))); |
64 Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|"))); |
65 |
65 |
66 val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs; |
66 val where_multi_specs = Parse.where_ |-- Parse.!!! multi_specs; |
67 |
67 |
68 |
68 |