changeset 46561 | 092f4eca9848 |
parent 46560 | 8e252a608765 |
child 46985 | bd955d9f464b |
--- a/src/HOL/Matrix/ComputeNumeral.thy Tue Feb 21 11:04:38 2012 +0100 +++ b/src/HOL/Matrix/ComputeNumeral.thy Tue Feb 21 11:08:05 2012 +0100 @@ -156,7 +156,7 @@ else apsnd uminus (posDivAlg (-a) (-b)))" by (auto simp only: divmod_int_def) -lemmas compute_div_mod = div_int_def mod_int_def divmod adjust posDivAlg.simps negDivAlg.simps +lemmas compute_div_mod = div_int_def mod_int_def divmod adjust apsnd_def map_pair_def posDivAlg.simps negDivAlg.simps