X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Futility%2Fstring.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Futility%2Fstring.ma;h=d2a55290124d6b60ac9ba2a317c6daf21f1aca62;hb=2d88fad67eb842ed5fc70cd435f9920c7a2583f8;hp=227f9f478d2cb285d09c501be7cc7e712ded1371;hpb=c515405206bfeb9f99d3e175b7f1e390ba299f28;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/utility/string.ma b/helm/software/matita/contribs/ng_assembly/utility/string.ma
index 227f9f478..d2a552901 100644
--- a/helm/software/matita/contribs/ng_assembly/utility/string.ma
+++ b/helm/software/matita/contribs/ng_assembly/utility/string.ma
@@ -21,7 +21,8 @@
 (* ********************************************************************** *)
 
 include "utility/ascii.ma".
-include "utility/utility.ma".
+include "freescale/theory.ma".
+include "freescale/nat.ma".
 
 (* ************************ *)
 (* MANIPOLAZIONE DI STRINGA *)
@@ -30,14 +31,6 @@ include "utility/utility.ma".
 (* tipo pubblico *)
 ndefinition aux_str_type ≝ list ascii.
 
-(* empty string *)
-ndefinition empty_str ≝ nil ascii.
-
-(* is empty ? *)
-ndefinition isNull_str ≝
-λstr:aux_str_type.match str with
- [ nil ⇒ true | cons _ _ ⇒ false ].
-
 (* strcmp *)
 nlet rec eq_str (str,str':aux_str_type) ≝
  match str with
@@ -50,13 +43,6 @@ nlet rec eq_str (str,str':aux_str_type) ≝
    ]
   ].
 
-(* strcat *)
-ndefinition strCat_str ≝
-λstr,str':aux_str_type.str@str'.
-
-(* strlen *)
-ndefinition strLen_str ≝ len_list ascii.
-
 (* ************ *)
 (* STRINGA + ID *)
 (* ************ *)