| changeset 30496 | 7cdcc9dd95cb |
| parent 30273 | ecd6f0ca62ea |
| child 30652 | 752329615264 |
--- a/src/HOL/Int.thy Thu Mar 12 18:01:25 2009 +0100 +++ b/src/HOL/Int.thy Thu Mar 12 18:01:26 2009 +0100 @@ -1527,7 +1527,7 @@ use "~~/src/Provers/Arith/assoc_fold.ML" use "Tools/int_arith.ML" -declaration {* K int_arith_setup *} +declaration {* K Int_Arith.setup *} subsection{*Lemmas About Small Numerals*}