1.1 --- a/src/HOL/NSA/NSA.thy	Thu Nov 17 07:31:37 2011 +0100
     1.2 +++ b/src/HOL/NSA/NSA.thy	Thu Nov 17 07:55:09 2011 +0100
     1.3 @@ -646,48 +646,20 @@
     1.4  lemma approx_trans3: "[| x @= r; x @= s|] ==> r @= s"
     1.5  by (blast intro: approx_sym approx_trans)
     1.6  
     1.7 -lemma number_of_approx_reorient: "(number_of w @= x) = (x @= number_of w)"
     1.8 +lemma approx_reorient: "(x @= y) = (y @= x)"
     1.9  by (blast intro: approx_sym)
    1.10  
    1.11 -lemma zero_approx_reorient: "(0 @= x) = (x @= 0)"
    1.12 -by (blast intro: approx_sym)
    1.13 -
    1.14 -lemma one_approx_reorient: "(1 @= x) = (x @= 1)"
    1.15 -by (blast intro: approx_sym)
    1.16 -
    1.17 -
    1.18 -ML {*
    1.19 -local
    1.20 -(*** re-orientation, following HOL/Integ/Bin.ML
    1.21 -     We re-orient x @=y where x is 0, 1 or a numeral, unless y is as well!
    1.22 - ***)
    1.23 -
    1.24 -(*reorientation simprules using ==, for the following simproc*)
    1.25 -val meta_zero_approx_reorient = @{thm zero_approx_reorient} RS eq_reflection;
    1.26 -val meta_one_approx_reorient = @{thm one_approx_reorient} RS eq_reflection;
    1.27 -val meta_number_of_approx_reorient = @{thm number_of_approx_reorient} RS eq_reflection
    1.28 -
    1.29  (*reorientation simplification procedure: reorients (polymorphic)
    1.30    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
    1.31 -fun reorient_proc sg _ (_ $ t $ u) =
    1.32 -  case u of
    1.33 -      Const(@{const_name Groups.zero}, _) => NONE
    1.34 -    | Const(@{const_name Groups.one}, _) => NONE
    1.35 -    | Const(@{const_name Int.number_of}, _) $ _ => NONE
    1.36 -    | _ => SOME (case t of
    1.37 -                Const(@{const_name Groups.zero}, _) => meta_zero_approx_reorient
    1.38 -              | Const(@{const_name Groups.one}, _) => meta_one_approx_reorient
    1.39 -              | Const(@{const_name Int.number_of}, _) $ _ =>
    1.40 -                                 meta_number_of_approx_reorient);
    1.41 -
    1.42 -in
    1.43 -
    1.44 -val approx_reorient_simproc = Simplifier.simproc_global @{theory}
    1.45 -  "reorient_simproc" ["0@=x", "1@=x", "number_of w @= x"] reorient_proc;
    1.46 -
    1.47 -end;
    1.48 -
    1.49 -Addsimprocs [approx_reorient_simproc];
    1.50 +simproc_setup approx_reorient_simproc
    1.51 +  ("0 @= x" | "1 @= y" | "number_of w @= z") =
    1.52 +{*
    1.53 +  let val rule = @{thm approx_reorient} RS eq_reflection
    1.54 +      fun proc phi ss ct = case term_of ct of
    1.55 +          _ $ t $ u => if can HOLogic.dest_number u then NONE
    1.56 +            else if can HOLogic.dest_number t then SOME rule else NONE
    1.57 +        | _ => NONE
    1.58 +  in proc end
    1.59  *}
    1.60  
    1.61  lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"