# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1357806505 0
# Node ID ea63068847aa742780acd0071b7ba10db666e6b7
# Parent  cb8754a0568a556d219071d4c48cd87a11b0f5a7
update

diff -r cb8754a0568a -r ea63068847aa Paper.thy
--- 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