src/HOL/Int.thy

--- a/src/HOL/Int.thy	Wed Apr 29 13:36:29 2009 -0700
+++ b/src/HOL/Int.thy	Wed Apr 29 17:15:01 2009 -0700
@@ -1518,6 +1518,13 @@
 use "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}
 
+setup {*
+  ReorientProc.add
+    (fn Const(@{const_name number_of}, _) $ _ => true | _ => false)
+*}
+
+simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc
+
 
 subsection{*Lemmas About Small Numerals*}