# HG changeset patch
# User haftmann
# Date 1246285075 -7200
# Node ID 4d278bbb5cc8176bd36e65655b20dbc294e9a4ce
# Parent  50b307148dab4a33d33fd73624842eb39854b9e8
tuned

diff -r 50b307148dab -r 4d278bbb5cc8 src/HOL/MicroJava/BV/BVExample.thy
--- 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)"