diff -r 46048223e0f9 -r b46ccfee8e59 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Wed Jul 14 13:32:21 1999 +0200
+++ b/src/HOL/Divides.ML	Thu Jul 15 10:27:54 1999 +0200
@@ -97,7 +97,7 @@
 (*** Quotient ***)
 
 Goal "(%m. m div n) = wfrec (trancl pred_nat) \
-                        \            (%f j. if j<n then 0 else Suc (f (j-n)))";
+\            (%f j. if j<n then 0 else Suc (f (j-n)))";
 by (simp_tac (simpset() addsimps [div_def]) 1);
 qed "div_eq";
 
@@ -116,7 +116,6 @@
 by (asm_simp_tac (simpset() addsimps [div_geq, not_less_iff_le]) 1);
 qed "le_div_geq";
 
-(*NOT suitable for rewriting: loops*)
 Goal "0<n ==> m div n = (if m<n then 0 else Suc((m-n) div n))";
 by (asm_simp_tac (simpset() addsimps [div_less, div_geq]) 1);
 qed "div_if";
@@ -306,7 +305,7 @@
 
 (*** More division laws ***)
 
-Goal "0<n ==> m*n div n = m";
+Goal "0<n ==> (m*n) div n = m";
 by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
 by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);