# HG changeset patch
# User huffman
# Date 1241053036 25200
# Node ID 6d2188134536e38439731ef8ac763063f8fe71cc
# Parent  0fdf666e08bf955639a0b63951b111ffde705f74
reorient simproc for unsigned numerals

diff -r 0fdf666e08bf -r 6d2188134536 src/HOL/ex/Numeral.thy
--- a/src/HOL/ex/Numeral.thy	Wed Apr 29 17:15:01 2009 -0700
+++ b/src/HOL/ex/Numeral.thy	Wed Apr 29 17:57:16 2009 -0700
@@ -909,7 +909,22 @@
 thm numeral
 
 
-text {* Toy examples *}
+subsection {* Simplification Procedures *}
+
+text {* Reorientation of equalities *}
+
+setup {*
+  ReorientProc.add
+    (fn Const(@{const_name of_num}, _) $ _ => true
+      | Const(@{const_name uminus}, _) $
+          (Const(@{const_name of_num}, _) $ _) => true
+      | _ => false)
+*}
+
+simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = ReorientProc.proc
+
+
+subsection {* Toy examples *}
 
 definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
 code_thms bar