1.1 --- a/src/HOL/ex/Numeral.thy	Wed Apr 29 17:15:01 2009 -0700
     1.2 +++ b/src/HOL/ex/Numeral.thy	Wed Apr 29 17:57:16 2009 -0700
     1.3 @@ -909,7 +909,22 @@
     1.4  thm numeral
     1.5  
     1.6  
     1.7 -text {* Toy examples *}
     1.8 +subsection {* Simplification Procedures *}
     1.9 +
    1.10 +text {* Reorientation of equalities *}
    1.11 +
    1.12 +setup {*
    1.13 +  ReorientProc.add
    1.14 +    (fn Const(@{const_name of_num}, _) $ _ => true
    1.15 +      | Const(@{const_name uminus}, _) $
    1.16 +          (Const(@{const_name of_num}, _) $ _) => true
    1.17 +      | _ => false)
    1.18 +*}
    1.19 +
    1.20 +simproc_setup reorient_num ("of_num n = x" | "- of_num m = y") = ReorientProc.proc
    1.21 +
    1.22 +
    1.23 +subsection {* Toy examples *}
    1.24  
    1.25  definition "bar \<longleftrightarrow> #4 * #2 + #7 = (#8 :: nat) \<and> #4 * #2 + #7 \<ge> (#8 :: int) - #3"
    1.26  code_thms bar