src/HOL/NSA/NSA.thy
changeset 39159 0dec18004e75
parent 37887 2ae085b07f2f
child 41541 1fa4725c4656
     1.1 --- a/src/HOL/NSA/NSA.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/NSA/NSA.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -663,9 +663,9 @@
     1.4   ***)
     1.5  
     1.6  (*reorientation simprules using ==, for the following simproc*)
     1.7 -val meta_zero_approx_reorient = thm "zero_approx_reorient" RS eq_reflection;
     1.8 -val meta_one_approx_reorient = thm "one_approx_reorient" RS eq_reflection;
     1.9 -val meta_number_of_approx_reorient = thm "number_of_approx_reorient" RS eq_reflection
    1.10 +val meta_zero_approx_reorient = @{thm zero_approx_reorient} RS eq_reflection;
    1.11 +val meta_one_approx_reorient = @{thm one_approx_reorient} RS eq_reflection;
    1.12 +val meta_number_of_approx_reorient = @{thm number_of_approx_reorient} RS eq_reflection
    1.13  
    1.14  (*reorientation simplification procedure: reorients (polymorphic)
    1.15    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)