# HG changeset patch
# User nipkow
# Date 1516009601 -3600
# Node ID a6bf7167c5e19f51ead105d25a7f69e6796eba2f
# Parent  e446505a4ec61606061eac6902426688d49f0e0f
tuned

diff -r e446505a4ec6 -r a6bf7167c5e1 src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Sun Jan 14 21:25:43 2018 +0100
+++ b/src/HOL/IMP/Collecting_Examples.thy	Mon Jan 15 10:46:41 2018 +0100
@@ -31,10 +31,12 @@
 
 definition "c0 = WHILE Less (V ''x'') (N 3)
                 DO ''x'' ::= Plus (V ''x'') (N 2)"
-definition C0 :: "state set acom" where "C0 = annotate (%p. {}) c0"
+
+definition C0 :: "state set acom" where "C0 = annotate (\<lambda>p. {}) c0"
 
 text\<open>Collecting semantics:\<close>
 
+value "show_acom (((step {<>}) ^^ 0) C0)"
 value "show_acom (((step {<>}) ^^ 1) C0)"
 value "show_acom (((step {<>}) ^^ 2) C0)"
 value "show_acom (((step {<>}) ^^ 3) C0)"