--- a/abacus.thy	Fri Jan 11 13:18:33 2013 +0000
+++ b/abacus.thy	Sat Jan 12 01:05:01 2013 +0000
@@ -177,6 +177,7 @@
              (L, 7), (W0, 5), (R, 6), (W0, 5), (W1, 3), (R, 6),
              (L, 8), (L, 7), (R, 9), (L, 7), (R, 10), (W0, 9)]" 
 
+(*  FIXME: doubly defined
 text {*
   @{text "tshift tm off"} shifts @{text "tm"} by offset @{text "off"}, leaving 
   instructions concerning state @{text "0"} unchanged, because state @{text "0"} 
@@ -188,6 +189,7 @@
   "tshift tp off = (map (\<lambda> (action, state). 
        (action, (if state = 0 then 0
                  else state + off))) tp)"
+*)
 
 text {*
   @{text "tinc ss n"} returns the TM which simulates the execution of