diff -r 40f414b87655 -r 366d4d234814 src/HOL/IntArith.thy --- a/src/HOL/IntArith.thy Mon Jul 30 19:46:15 2007 +0200 +++ b/src/HOL/IntArith.thy Tue Jul 31 00:56:26 2007 +0200 @@ -115,7 +115,7 @@ min_def[of "number_of u" "1::int", standard, simp] use "int_arith1.ML" -setup int_arith_setup +declaration {* K int_arith_setup *} subsection{*Lemmas About Small Numerals*}