src/HOL/Quickcheck_Narrowing.thy
changeset 48253 4410a709913c
parent 47108 2a1953f0d20d
child 48565 7c497a239007
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jul 12 21:46:11 2012 +1000
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jul 12 16:22:33 2012 +0200
     1.3 @@ -138,10 +138,6 @@
     1.4    [code del]: "div_mod n m = (n div m, n mod m)"
     1.5  
     1.6  lemma [code]:
     1.7 -  "div_mod n m = (if m = 0 then (0, n) else (n div m, n mod m))"
     1.8 -  unfolding div_mod_def by auto
     1.9 -
    1.10 -lemma [code]:
    1.11    "n div m = fst (div_mod n m)"
    1.12    unfolding div_mod_def by simp
    1.13