# HG changeset patch
# User haftmann
# Date 1561143300 0
# Node ID 9497a6334a26752d09d58b7b934d639ea8f9e846
# Parent  7aa64296b9b06e381da9123f1223d615838ea56a
tuned

diff -r 7aa64296b9b0 -r 9497a6334a26 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Jun 16 16:40:57 2019 +0000
+++ b/src/HOL/Int.thy	Fri Jun 21 18:55:00 2019 +0000
@@ -1086,7 +1086,7 @@
 
 subsection \<open>Setting up simplification procedures\<close>
 
-lemmas of_int_simps =
+lemmas of_int_simps [no_atp] =
   of_int_0 of_int_1 of_int_add of_int_mult
 
 ML_file \<open>Tools/int_arith.ML\<close>