equal
deleted
inserted
replaced
217 in |
217 in |
218 Local_Theory.note (bind', simps) lthy |> snd |
218 Local_Theory.note (bind', simps) lthy |> snd |
219 end |
219 end |
220 |
220 |
221 val _ = |
221 val _ = |
222 Outer_Syntax.local_theory @{command_spec "case_of_simps"} |
222 Outer_Syntax.local_theory @{command_keyword case_of_simps} |
223 "turn a list of equations into a case expression" |
223 "turn a list of equations into a case expression" |
224 (Parse_Spec.opt_thm_name ":" -- Parse.xthms1 >> case_of_simps_cmd) |
224 (Parse_Spec.opt_thm_name ":" -- Parse.xthms1 >> case_of_simps_cmd) |
225 |
225 |
226 val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |-- |
226 val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |-- |
227 Parse.xthms1 --| @{keyword ")"} |
227 Parse.xthms1 --| @{keyword ")"} |
228 |
228 |
229 val _ = |
229 val _ = |
230 Outer_Syntax.local_theory @{command_spec "simps_of_case"} |
230 Outer_Syntax.local_theory @{command_keyword simps_of_case} |
231 "perform case split on rule" |
231 "perform case split on rule" |
232 (Parse_Spec.opt_thm_name ":" -- Parse.xthm -- |
232 (Parse_Spec.opt_thm_name ":" -- Parse.xthm -- |
233 Scan.optional parse_splits [] >> simps_of_case_cmd) |
233 Scan.optional parse_splits [] >> simps_of_case_cmd) |
234 |
234 |
235 end |
235 end |