equal
deleted
inserted
replaced
106 >> Element.Defines || |
106 >> Element.Defines || |
107 P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1)) |
107 P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1)) |
108 >> (curry Element.Notes ""); |
108 >> (curry Element.Notes ""); |
109 |
109 |
110 fun plus1_unless test scan = |
110 fun plus1_unless test scan = |
111 scan -- Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)) >> op ::; |
111 scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)); |
112 |
112 |
113 val rename = P.name -- Scan.option P.mixfix; |
113 val rename = P.name -- Scan.option P.mixfix; |
114 |
114 |
115 in |
115 in |
116 |
116 |