--- a/Paper.thy	Thu Jan 10 08:27:42 2013 +0000
+++ b/Paper.thy	Thu Jan 10 08:28:25 2013 +0000
@@ -37,8 +37,10 @@
 done
 
 lemma tstep_def2:
-  shows "tstep (s, l, []) p = (let (ac, ns) = fetch p s Bk in (ns, new_tape ac (l, [])))"
-  and "tstep (s, l, x#xs) p = (let (ac, ns) = fetch p s x in (ns, new_tape ac (l, x#xs)))"
+  shows "tstep (s, l, []) p == (let (ac, ns) = fetch p s Bk in (ns, new_tape ac (l, [])))"
+  and "tstep (s, l, x#xs) p == (let (ac, ns) = fetch p s x in (ns, new_tape ac (l, x#xs)))"
+apply -
+apply(rule_tac [!] eq_reflection)
 by (auto split: prod.split list.split simp add: tstep.simps)
 
 consts DUMMY::'a