tuned message;
authorwenzelm
Wed, 23 Jul 2014 23:16:44 +0200
changeset 57628 c80fc5576271
parent 57627 65fc7ae1bf66
child 57629 e88b5f59cade
tuned message;
src/HOL/Library/simps_case_conv.ML
--- 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 ":"} |--