Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove "safe" (as suggested by Tobias) and added "arith" to "try"
authorblanchet
Wed, 08 Sep 2010 15:57:50 +0200
changeset 39222 decf607a5a67
parent 39221 70fd4a3c41ed
child 39223 022f16801e4e
remove "safe" (as suggested by Tobias) and added "arith" to "try"
src/HOL/Tools/try.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/try.ML	Mon Sep 06 17:51:26 2010 +0200
+++ b/src/HOL/Tools/try.ML	Wed Sep 08 15:57:50 2010 +0200
@@ -51,9 +51,9 @@
                       else "")) I (#goal o Proof.goal)
              (apply_named_method_on_first_goal name (Proof.context_of st)) st
 
-val all_goals_named_methods = ["auto", "safe"]
+val all_goals_named_methods = ["auto"]
 val first_goal_named_methods =
-  ["simp", "fast", "fastsimp", "force", "best", "blast"]
+  ["simp", "fast", "fastsimp", "force", "best", "blast", "arith"]
 val do_methods =
   map do_named_method_on_first_goal all_goals_named_methods @
   map do_named_method first_goal_named_methods
isabelle