# HG changeset patch
# User huffman
# Date 1333115772 -7200
# Node ID ea712316fc871b424b4a1cf530d7c90042a4eed0
# Parent  65031898155705705409ebfbe7b8cbb770701e81
set up numeral reorient simproc in Num.thy

diff -r 650318981557 -r ea712316fc87 src/HOL/Int.thy
--- 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*}
 
diff -r 650318981557 -r ea712316fc87 src/HOL/Num.thy
--- 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. *}