diff -r 64eda8afe2b4 -r 3d5b2b874e14 Arith.ML
--- a/Arith.ML	Tue Feb 15 10:05:17 1994 +0100
+++ b/Arith.ML	Wed Feb 16 15:13:53 1994 +0100
@@ -126,12 +126,6 @@
 by (rtac refl 1);
 val less_eq = result();
 
-(*
-val div_simps = [div_termination, cut_apply, less_eq];
-val div_ss = nat_ss addsimps div_simps;
-val div_ss = nat_ss addsimps div_simps;
-*)
-
 goal Arith.thy "!!m. m<n ==> m mod n = m";
 by (rtac (mod_def RS wf_less_trans) 1);
 by(asm_simp_tac HOL_ss 1);