Mercurial Mercurial > hg > tm / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Sat, 19 Jan 2013 12:46:28 +0000
changeset 53 25b1633a278d
parent 52 2cb1e4499983
child 54 e7d845acb0a7
tuned
thys/turing_basic.thy file | annotate | diff | comparison | revisions 
--- 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
tm