tuned
authorhaftmann
Fri Jun 21 18:55:00 2019 +0000 (4 weeks ago)
changeset 703549497a6334a26
parent 70353 7aa64296b9b0
child 70355 a80ad0ac0837
tuned
src/HOL/Int.thy
     1.1 --- a/src/HOL/Int.thy	Sun Jun 16 16:40:57 2019 +0000
     1.2 +++ b/src/HOL/Int.thy	Fri Jun 21 18:55:00 2019 +0000
     1.3 @@ -1086,7 +1086,7 @@
     1.4  
     1.5  subsection \<open>Setting up simplification procedures\<close>
     1.6  
     1.7 -lemmas of_int_simps =
     1.8 +lemmas of_int_simps [no_atp] =
     1.9    of_int_0 of_int_1 of_int_add of_int_mult
    1.10  
    1.11  ML_file \<open>Tools/int_arith.ML\<close>