diff -r 23eeaac32d21 -r e3ecf558aef2 thys/Hoare_tm.thy
--- a/thys/Hoare_tm.thy	Thu Apr 03 12:47:07 2014 +0100
+++ b/thys/Hoare_tm.thy	Thu Apr 03 12:55:43 2014 +0100
@@ -63,6 +63,7 @@
 *)
 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"
 
+(* updates the position/tape according to an action *)
 fun 
   next_tape :: "taction \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int \<rightharpoonup> Block))"
 where