equal
deleted
inserted
replaced
153 val setup = |
153 val setup = |
154 trace_eqvt_setup |
154 trace_eqvt_setup |
155 |
155 |
156 |
156 |
157 (** methods **) |
157 (** methods **) |
158 |
158 val _ = OuterKeyword.keyword "exclude" |
159 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
159 val add_thms_parser = Scan.optional (Scan.lift (Args.add -- Args.colon) |-- Attrib.thms) []; |
160 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
160 val exclude_consts_parser = Scan.optional (Scan.lift ((Args.$$$ "exclude") -- Args.colon) |-- |
161 (Scan.repeat (Args.const true))) [] |
161 (Scan.repeat (Args.const true))) [] |
162 |
162 |
163 val args_parser = add_thms_parser -- exclude_consts_parser |
163 val args_parser = add_thms_parser -- exclude_consts_parser |