X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fassembly%2Fexadecimal.ma;h=c059b43fa5fe91f079ff05b951157eb6559a9bb8;hb=6db38e3d8e4083765f2fce40c7845c9827b9afd0;hp=761c06c94718ce89014d63e06622198fad0d83ab;hpb=b348a1a39e17b541fca17d2218a3b91bd7f1fece;p=helm.git

diff --git a/helm/software/matita/library/assembly/exadecimal.ma b/helm/software/matita/library/assembly/exadecimal.ma
index 761c06c94..c059b43fa 100644
--- a/helm/software/matita/library/assembly/exadecimal.ma
+++ b/helm/software/matita/library/assembly/exadecimal.ma
@@ -768,8 +768,7 @@ lemma lt_nat_of_exadecimal_16: ∀b. nat_of_exadecimal b < 16.
  elim b;
  simplify;
  [
- |*: alias id "lt_S_S" = "cic:/matita/algebra/finite_groups/lt_S_S.con".
-   repeat (apply lt_S_S)
+ |*: repeat (apply lt_to_lt_S_S)
  ];
  autobatch.
 qed.