src/HOL/Num.thy
changeset 47226 ea712316fc87
parent 47220 52426c62b5d0
child 47227 bc18fa07053b
     1.1 --- a/src/HOL/Num.thy	Fri Mar 30 15:43:30 2012 +0200
     1.2 +++ b/src/HOL/Num.thy	Fri Mar 30 15:56:12 2012 +0200
     1.3 @@ -975,10 +975,6 @@
     1.4  
     1.5  subsection {* Setting up simprocs *}
     1.6  
     1.7 -lemma numeral_reorient:
     1.8 -  "(numeral w = x) = (x = numeral w)"
     1.9 -  by auto
    1.10 -
    1.11  lemma mult_numeral_1: "Numeral1 * a = (a::'a::semiring_numeral)"
    1.12    by simp
    1.13  
    1.14 @@ -999,6 +995,16 @@
    1.15    mult_numeral_1 mult_numeral_1_right 
    1.16    mult_minus1 mult_minus1_right
    1.17  
    1.18 +setup {*
    1.19 +  Reorient_Proc.add
    1.20 +    (fn Const (@{const_name numeral}, _) $ _ => true
    1.21 +    | Const (@{const_name neg_numeral}, _) $ _ => true
    1.22 +    | _ => false)
    1.23 +*}
    1.24 +
    1.25 +simproc_setup reorient_numeral
    1.26 +  ("numeral w = x" | "neg_numeral w = y") = Reorient_Proc.proc
    1.27 +
    1.28  
    1.29  subsubsection {* Simplification of arithmetic operations on integer constants. *}
    1.30