src/HOL/Tools/try.ML
changeset 39222 decf607a5a67
parent 38946 da5e4f182f69
child 39331 8b1969d603c0
equal deleted inserted replaced
39221:70fd4a3c41ed 39222:decf607a5a67
    49 fun do_named_method_on_first_goal name st =
    49 fun do_named_method_on_first_goal name st =
    50   do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
    50   do_generic (name ^ (if nprems_of (#goal (Proof.goal st)) > 1 then "[1]"
    51                       else "")) I (#goal o Proof.goal)
    51                       else "")) I (#goal o Proof.goal)
    52              (apply_named_method_on_first_goal name (Proof.context_of st)) st
    52              (apply_named_method_on_first_goal name (Proof.context_of st)) st
    53 
    53 
    54 val all_goals_named_methods = ["auto", "safe"]
    54 val all_goals_named_methods = ["auto"]
    55 val first_goal_named_methods =
    55 val first_goal_named_methods =
    56   ["simp", "fast", "fastsimp", "force", "best", "blast"]
    56   ["simp", "fast", "fastsimp", "force", "best", "blast", "arith"]
    57 val do_methods =
    57 val do_methods =
    58   map do_named_method_on_first_goal all_goals_named_methods @
    58   map do_named_method_on_first_goal all_goals_named_methods @
    59   map do_named_method first_goal_named_methods
    59   map do_named_method first_goal_named_methods
    60 
    60 
    61 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"
    61 fun time_string (s, ms) = s ^ ": " ^ string_of_int ms ^ " ms"