chore(builtin/num): remove leftover

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-02-09 11:39:26 -08:00 · 2014-02-09 11:39:26 -08:00 · 4c76f6abb9
commit 4c76f6abb9
parent 8df7c7b02d
2 changed files with 0 additions and 2 deletions
--- a/src/builtin/num.lean
+++ b/src/builtin/num.lean
@ -557,8 +557,6 @@ add_rewrite mul_onel mul_oner
 theorem mul_comm (a b : num) : a * b = b * a
 := induction_on b (by simp) (by simp)

-exit
-
 theorem distributer (a b c : num) : a * (b + c) = a * b + a * c
 := induction_on a (by simp) (by simp)

--- a/src/builtin/obj/num.olean
+++ b/src/builtin/obj/num.olean