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/uncomputable.thy
changeset 76 04399b471108
parent 71 8c7f10b3da7b
child 80 eb589fa73fc1 
--- a/thys/uncomputable.thy	Thu Jan 24 15:04:11 2013 +0100
+++ b/thys/uncomputable.thy	Thu Jan 24 17:14:39 2013 +0100
@@ -1070,10 +1070,10 @@
 
 (* invariants of dither *)
 abbreviation
-  "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc, Oc]"
+  "dither_halt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc, Oc]"
 
 abbreviation
-  "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>nd. l = Bk \<up> nd) \<and> r = [Oc]"
+  "dither_unhalt_inv \<equiv> \<lambda>(l, r). (\<exists>n. l = Bk \<up> n) \<and> r = [Oc]"
 
 lemma dither_unhalt_state: 
   "(steps0 (1, Bk \<up> m, [Oc]) dither stp = (1, Bk \<up> m, [Oc])) \<or>
tm