# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1358599588 0
# Node ID 25b1633a278d86deeedca002bab6e155f0c10aab
# Parent  2cb1e4499983ae14eb2bd25c87b1a49f8e585310
tuned

diff -r 2cb1e4499983 -r 25b1633a278d thys/turing_basic.thy
--- a/thys/turing_basic.thy	Sat Jan 19 12:45:14 2013 +0000
+++ b/thys/turing_basic.thy	Sat Jan 19 12:46:28 2013 +0000
@@ -223,12 +223,6 @@
       \<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
     and h: " steps (1, tp) A (Suc n) = (0, tp')"
     from h show  "\<exists>n'. \<not> is_final (steps (1, tp) A n') \<and> steps (1, tp) A (Suc n') = (0, tp')"
-      (*
-      apply(simp add: step_red del: steps.simps)
-      apply(case_tac "(steps (Suc 0, tp) A n)")
-      apply(case_tac "a = 0")
-      apply(simp)
-      *)
     proof(simp add: step_red del: steps.simps, 
                      case_tac "(steps (Suc 0, tp) A n)", case_tac "a = 0", simp)
       fix a b c