Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/scnp_reconstruct.ML
changeset 33569 1ebb8b7b9f6a
parent 33099 b8cdd3d73022
child 33578 0c3ba1e010d2 
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 29 12:50:44 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Oct 29 15:16:54 2009 +0100
@@ -197,7 +197,7 @@
               else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
           in
             rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
-            THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac)
+            THEN (if tag_flag then Arith_Data.arith_tac ctxt 1 else all_tac)
           end
 
         fun steps_tac MAX strict lq lp =
isabelle