# HG changeset patch
# User wenzelm
# Date 1406150204 -7200
# Node ID c80fc5576271a6d46d74a9325c291bb1d18a183a
# Parent  65fc7ae1bf662c341954c3ed415211cba92e9a5a
tuned message;

diff -r 65fc7ae1bf66 -r c80fc5576271 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 ":"} |--