src/HOL/Decision_Procs/approximation.ML
changeset 59936 b8ffc3dc9e24
parent 59850 f339ff48a6ee
child 59970 e9f73d87d904
     1.1 --- a/src/HOL/Decision_Procs/approximation.ML	Mon Apr 06 16:30:44 2015 +0200
     1.2 +++ b/src/HOL/Decision_Procs/approximation.ML	Mon Apr 06 17:06:48 2015 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4    Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
     1.5  
     1.6  val _ =
     1.7 -  Outer_Syntax.command @{command_spec "approximate"} "print approximation of term"
     1.8 +  Outer_Syntax.command @{command_keyword approximate} "print approximation of term"
     1.9      (opt_modes -- Parse.term
    1.10        >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t)));
    1.11