| changeset 24075 | 366d4d234814 |
| parent 23851 | 7921b81baf96 |
| child 24090 | ab6f04807005 |
--- 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*}