Mercurial Mercurial > repos > isabelle / 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
authorhaftmann
Mon, 29 Jun 2009 16:17:55 +0200
changeset 31867 4d278bbb5cc8
parent 31854 50b307148dab
child 31868 edd1f30c0477
tuned
src/HOL/MicroJava/BV/BVExample.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/MicroJava/BV/BVExample.thy	Mon Jun 29 14:55:08 2009 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Mon Jun 29 16:17:55 2009 +0200
@@ -450,7 +450,7 @@
 qed
 
 lemma [code]:
-  "iter f step ss w = while (\<lambda>(ss, w). \<not> (is_empty w))
+  "iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w)
     (\<lambda>(ss, w).
         let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p}))
     (ss, w)"
isabelle