X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fassembly%2Ffreescale%2Fexadecim.ma;h=3cfa1536a0a9a21801e3d8d8ed13fc8645f96a40;hb=45f87a7044ccab3d8f1300bfc33ca93a6ad868cb;hp=969c22a36a5ca9a0dac93394d89a14cfc03482a6;hpb=21f1fb39b5e1187ef87387f20522e60abe4f7c19;p=helm.git

diff --git a/helm/software/matita/contribs/assembly/freescale/exadecim.ma b/helm/software/matita/contribs/assembly/freescale/exadecim.ma
index 969c22a36..3cfa1536a 100644
--- a/helm/software/matita/contribs/assembly/freescale/exadecim.ma
+++ b/helm/software/matita/contribs/assembly/freescale/exadecim.ma
@@ -1558,7 +1558,7 @@ lemma lt_nat_of_exadecim_16: ∀e.nat_of_exadecim e < 16.
  intro;
  elim e;
  simplify;
- autobatch depth=17.
+ unfold;autobatch depth=17 size=20.
 qed.
 
 lemma exadecim_of_nat_mod:
@@ -1589,7 +1589,7 @@ lemma exadecim_of_nat_mod:
  rewrite < mod_mod;
   [ apply H;
     unfold lt;
-    autobatch.
+    autobatch depth=20 size=20.
   | autobatch
   ]
 qed.