From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 24 Apr 2007 15:06:19 +0000 (+0000)
Subject: goal ==> focus
X-Git-Tag: make_still_working~6360
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4e9f8c32689979faca3cfdc1692c1690fd789bfc;p=helm.git

goal ==> focus
---

diff --git a/helm/software/matita/library_auto/auto/nat/div_and_mod.ma b/helm/software/matita/library_auto/auto/nat/div_and_mod.ma
index 9b9be7cf2..215f387af 100644
--- a/helm/software/matita/library_auto/auto/nat/div_and_mod.ma
+++ b/helm/software/matita/library_auto/auto/nat/div_and_mod.ma
@@ -261,9 +261,11 @@ qed.
 (* some properties of div and mod *)
 theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
 intros.
-apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
-goal 15. (* ?11 is closed with the following tactics *)
-apply div_mod_spec_div_mod.auto.auto.
+apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O);
+[2: apply div_mod_spec_div_mod.auto.
+| skip
+| auto
+]
 (*unfold lt.apply le_S_S.apply le_O_n.
 apply div_mod_spec_times.*)
 qed.