src/HOL/Library/simps_case_conv.ML
changeset 59936 b8ffc3dc9e24
parent 59650 ba26118128b7
child 60354 235d65be79c9
     1.1 --- a/src/HOL/Library/simps_case_conv.ML	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/HOL/Library/simps_case_conv.ML	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4    end
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.local_theory @{command_spec "case_of_simps"}
     1.8 +  Outer_Syntax.local_theory @{command_keyword case_of_simps}
     1.9      "turn a list of equations into a case expression"
    1.10      (Parse_Spec.opt_thm_name ":"  -- Parse.xthms1 >> case_of_simps_cmd)
    1.11  
    1.12 @@ -227,7 +227,7 @@
    1.13    Parse.xthms1 --| @{keyword ")"}
    1.14  
    1.15  val _ =
    1.16 -  Outer_Syntax.local_theory @{command_spec "simps_of_case"}
    1.17 +  Outer_Syntax.local_theory @{command_keyword simps_of_case}
    1.18      "perform case split on rule"
    1.19      (Parse_Spec.opt_thm_name ":"  -- Parse.xthm --
    1.20        Scan.optional parse_splits [] >> simps_of_case_cmd)