X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fassembly%2Fexadecimal.ma;h=fb1a14ede914299c6b2e9342296e846c39dc54b0;hb=dfbd010fe5a46d049849913bc23000289893ea4f;hp=7dfd42bb117af8111b6efd1ee1c81a3242c5a709;hpb=754906e075ef350423de1e7fd3a7ac71bea53848;p=helm.git diff --git a/matita/library/assembly/exadecimal.ma b/matita/library/assembly/exadecimal.ma index 7dfd42bb1..fb1a14ede 100644 --- a/matita/library/assembly/exadecimal.ma +++ b/matita/library/assembly/exadecimal.ma @@ -14,7 +14,7 @@ set "baseuri" "cic:/matita/assembly/exadecimal/". -include "extra.ma". +include "assembly/extra.ma". inductive exadecimal : Type ≝ x0: exadecimal @@ -927,4 +927,4 @@ lemma xpred_S: ∀b. xpred (exadecimal_of_nat (S b)) = exadecimal_of_nat b. intros; rewrite > exadecimal_of_nat_mod; rewrite > exadecimal_of_nat_mod in ⊢ (? ? ? %); -*) \ No newline at end of file +*)