--- a/thys/Hoare_tm.thy	Thu Mar 27 15:12:33 2014 +0000
+++ b/thys/Hoare_tm.thy	Thu Apr 03 12:47:07 2014 +0100
@@ -31,7 +31,8 @@
   {* Scan.succeed (SIMPLE_METHOD' o (K (K prune_params_tac))) *} 
   "pruning parameters"
 
-lemma int_add_C :"x + (y::int) = y + x"
+lemma int_add_C: 
+  "x + (y::int) = y + x"
   by simp
 
 lemma int_add_A : "(x + y) + z = x + (y + (z::int))"
@@ -51,14 +52,14 @@
 
 datatype Block = Oc | Bk
 
-(* the successor state when tape symbol is Bk or Oc, respectively*)
+(* the successor state when tape symbol is Bk or Oc, respectively *)
 type_synonym tm_inst = "(taction \<times> tstate) \<times> (taction \<times> tstate)"
 
-(* - number of faults
-   - TM program
-   - current state
-   - position of head
-   - tape
+(* - number of faults (nat)
+   - TM program (nat \<rightharpoonup> tm_inst)
+   - current state (nat)
+   - position of head (int)
+   - tape (int \<rightharpoonup> Block)
 *)
 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)"