Modifications and refactoring

[helm.git] / matita / matita / lib / turing / universal / marks.ma

diff --git a/matita/matita/lib/turing/universal/marks.ma b/matita/matita/lib/turing/universal/marks.ma
index 13e85c56d0a311792630b16808906a3d62d948c0..829f56dc57ea7c1a2f80eef71df3a2d60a399ce4 100644 (file)
--- a/matita/matita/lib/turing/universal/marks.ma
+++ b/matita/matita/lib/turing/universal/marks.ma
@@ -443,10 +443,6 @@ qed.
         ^
 *)
 
-definition is_marked ≝ 
-  λalpha.λp:FinProd … alpha FinBool.
-  let 〈x,b〉 ≝ p in b.
-
 definition adv_both_marks ≝ 
   λalpha.seq ? (adv_mark_r alpha)
     (seq ? (move_l ?)