# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1547126287 0
# Node ID 3fee65a4083836f717b2496efeab3a471802025f
# Parent  fa6f654cbc134fbc66ac60275d311f9b7bea879a
updated to Isabelle 2018

diff -r fa6f654cbc13 -r 3fee65a40838 thys2/Recs.thy
--- a/thys2/Recs.thy	Thu Jan 10 13:00:04 2019 +0000
+++ b/thys2/Recs.thy	Thu Jan 10 13:18:07 2019 +0000
@@ -533,11 +533,7 @@
 
 lemma Quo_div: 
   shows "Quo x y = y div x"
-apply(case_tac "x = 0")
-apply(simp add: Quo0)
-apply(subst split_div_lemma[symmetric])
-apply(auto intro: Quo1 Quo4)
-done
+by (metis Quo0 Quo1 Quo4 div_by_0 div_nat_eqI mult_Suc_right neq0_conv)
 
 lemma Quo_rec_quo:
   shows "rec_eval rec_quo [y, x] = Quo x y"