src/HOL/Int.thy
changeset 31024 0fdf666e08bf
parent 31021 53642251a04f
child 31065 d87465cbfc9e
     1.1 --- a/src/HOL/Int.thy	Wed Apr 29 13:36:29 2009 -0700
     1.2 +++ b/src/HOL/Int.thy	Wed Apr 29 17:15:01 2009 -0700
     1.3 @@ -1518,6 +1518,13 @@
     1.4  use "Tools/int_arith.ML"
     1.5  declaration {* K Int_Arith.setup *}
     1.6  
     1.7 +setup {*
     1.8 +  ReorientProc.add
     1.9 +    (fn Const(@{const_name number_of}, _) $ _ => true | _ => false)
    1.10 +*}
    1.11 +
    1.12 +simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc
    1.13 +
    1.14  
    1.15  subsection{*Lemmas About Small Numerals*}
    1.16