--- a/src/HOL/Int.thy Fri Mar 30 15:43:30 2012 +0200
+++ b/src/HOL/Int.thy Fri Mar 30 15:56:12 2012 +0200
@@ -844,16 +844,6 @@
"(m::'a::linordered_idom) = n") =
{* fn _ => fn ss => fn ct => Lin_Arith.simproc ss (term_of ct) *}
-setup {*
- Reorient_Proc.add
- (fn Const (@{const_name numeral}, _) $ _ => true
- | Const (@{const_name neg_numeral}, _) $ _ => true
- | _ => false)
-*}
-
-simproc_setup reorient_numeral
- ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
-
subsection{*Lemmas About Small Numerals*}
--- a/src/HOL/Num.thy Fri Mar 30 15:43:30 2012 +0200
+++ b/src/HOL/Num.thy Fri Mar 30 15:56:12 2012 +0200
@@ -975,10 +975,6 @@
subsection {* Setting up simprocs *}
-lemma numeral_reorient:
- "(numeral w = x) = (x = numeral w)"
- by auto
-
lemma mult_numeral_1: "Numeral1 * a = (a::'a::semiring_numeral)"
by simp
@@ -999,6 +995,16 @@
mult_numeral_1 mult_numeral_1_right
mult_minus1 mult_minus1_right
+setup {*
+ Reorient_Proc.add
+ (fn Const (@{const_name numeral}, _) $ _ => true
+ | Const (@{const_name neg_numeral}, _) $ _ => true
+ | _ => false)
+*}
+
+simproc_setup reorient_numeral
+ ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
+
subsubsection {* Simplification of arithmetic operations on integer constants. *}