author | haftmann |
Fri, 21 Jun 2019 18:55:00 +0000 | |
changeset 70354 | 9497a6334a26 |
parent 70353 | 7aa64296b9b0 |
child 70355 | a80ad0ac0837 |
src/HOL/Int.thy | file | annotate | diff | comparison | revisions |
--- 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>