author | wenzelm |
Wed, 23 Jul 2014 23:16:44 +0200 | |
changeset 57628 | c80fc5576271 |
parent 57627 | 65fc7ae1bf66 |
child 57629 | e88b5f59cade |
--- a/src/HOL/Library/simps_case_conv.ML Wed Jul 23 23:08:22 2014 +0200 +++ b/src/HOL/Library/simps_case_conv.ML Wed Jul 23 23:16:44 2014 +0200 @@ -220,7 +220,7 @@ val _ = Outer_Syntax.local_theory @{command_spec "case_of_simps"} - "turns a list of equations into a case expression" + "turn a list of equations into a case expression" (Parse_Spec.opt_thm_name ":" -- Parse_Spec.xthms1 >> case_of_simps_cmd) val parse_splits = @{keyword "("} |-- Parse.reserved "splits" |-- @{keyword ":"} |--