Modifications and refactoring

[helm.git] / matita / matita / lib / turing / basic_machines.ma

diff --git a/matita/matita/lib/turing/basic_machines.ma b/matita/matita/lib/turing/basic_machines.ma
index 796992e22efd37257685b08b780830da63cc4f18..eed6ad1f670c51a1d9bfecc732477e2e95753206 100644 (file)
--- a/matita/matita/lib/turing/basic_machines.ma
+++ b/matita/matita/lib/turing/basic_machines.ma
@@ -199,7 +199,7 @@ definition swap ≝
  mk_TM alpha (swap_states alpha)
  (λp.let 〈q,a〉 ≝ p in
   let 〈q',b〉 ≝ q in
-  let q' ≝ pi1 nat (λi.i<4) q' in (* perche' devo passare il predicato ??? *)
+  let q' ≝ pi1 nat (λi.i<4) q' in
   match a with 
   [ None ⇒ 〈〈swap3,foo〉,None ?〉 (* if tape is empty then stop *)
   | Some a' ⇒