Mercurial Mercurial > hg > tm / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/turing_basic.thy
changeset 50 816e84ca16d6
parent 47 251e192339b7
child 51 6725c9c026f6 
--- a/thys/turing_basic.thy	Fri Jan 18 13:03:09 2013 +0000
+++ b/thys/turing_basic.thy	Fri Jan 18 13:56:35 2013 +0000
@@ -71,7 +71,7 @@
 fun step :: "config \<Rightarrow> tprog \<Rightarrow> config"
   where 
   "step (s, l, r) (p, off) = 
-  (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))"
+     (let (a, s') = fetch p (s - off) (read r) in (s', update a (l, r)))"
 
 fun steps :: "config \<Rightarrow> tprog \<Rightarrow> nat \<Rightarrow> config"
   where
@@ -93,7 +93,6 @@
                     (\<forall>(a, s) \<in> set p. s \<le> length p div 2
                                              + off \<and> s \<ge> off))"
 
-(* FIXME: needed? *)
 lemma halt_lemma: 
   "\<lbrakk>wf LE; \<forall>n. (\<not> P (f n) \<longrightarrow> (f (Suc n), (f n)) \<in> LE)\<rbrakk> \<Longrightarrow> \<exists>n. P (f n)"
 by (metis wf_iff_no_infinite_down_chain)
tm