src/HOL/Rat.thy
changeset 55143 04448228381d
parent 54863 82acc20ded73
child 55974 c835a9379026
     1.1 --- a/src/HOL/Rat.thy	Sat Jan 25 21:52:04 2014 +0100
     1.2 +++ b/src/HOL/Rat.thy	Sat Jan 25 22:06:07 2014 +0100
     1.3 @@ -622,8 +622,8 @@
     1.4      (* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *)
     1.5    #> Lin_Arith.add_simps [@{thm neg_less_iff_less},
     1.6        @{thm True_implies_equals},
     1.7 -      read_instantiate @{context} [(("a", 0), "(numeral ?v)")] @{thm distrib_left},
     1.8 -      read_instantiate @{context} [(("a", 0), "(- numeral ?v)")] @{thm distrib_left},
     1.9 +      @{thm distrib_left [where a = "numeral v" for v]},
    1.10 +      @{thm distrib_left [where a = "- numeral v" for v]},
    1.11        @{thm divide_1}, @{thm divide_zero_left},
    1.12        @{thm times_divide_eq_right}, @{thm times_divide_eq_left},
    1.13        @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym,