diff -r 087d82632852 -r e04123f4bacc thys/Hoare_tm3.thy
--- a/thys/Hoare_tm3.thy	Tue Apr 29 15:26:48 2014 +0100
+++ b/thys/Hoare_tm3.thy	Fri May 30 12:04:49 2014 +0100
@@ -47,26 +47,27 @@
 
 section {* Operational Semantics of TM *}
 
-datatype taction = W0 | W1 | L | R
-
-type_synonym tstate = nat
-
+datatype action = W0 | W1 | L | R
+
+type_synonym state = nat
+
+(* FIXME: I think Block should be changed to cell *)
 datatype Block = Oc | Bk
 
 (* the successor state when tape symbol is Bk or Oc, respectively *)
-type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"
+type_synonym tm_inst = "(action \<times> state) \<times> (action \<times> state)"
 
 (* - number of faults (nat)
-   - TM program (nat \<rightharpoonup> tm_inst)
+   - TM program (nat f\<rightharpoonup> tm_inst)
    - current state (nat)
    - position of head (int)
-   - tape (int \<rightharpoonup> Block)
+   - tape (int f\<rightharpoonup> Block)
 *)
 type_synonym tconf = "nat \<times> (nat f\<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int f\<rightharpoonup> Block)"
 
 (* updates the position/tape according to an action *)
 fun 
-  next_tape :: "taction \<Rightarrow> (int \<times>  (int f\<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int f\<rightharpoonup> Block))"
+  next_tape :: "action \<Rightarrow> (int \<times>  (int f\<rightharpoonup> Block)) \<Rightarrow> (int \<times>  (int f\<rightharpoonup> Block))"
 where 
   "next_tape W0 (pos, m) = (pos, m(pos f\<mapsto> Bk))" |
   "next_tape W1 (pos, m) = (pos, m(pos f\<mapsto> Oc))" |