# HG changeset patch
# User nipkow
# Date 1357637659 -3600
# Node ID d5c07ddd929be1e6a425f1263ee9690753a747e5
# Parent  ba79e2cb3cbee6d01fa104c8fccbbff62542171c
tuned names

diff -r ba79e2cb3cbe -r d5c07ddd929b src/HOL/IMP/Collecting_Examples.thy
--- a/src/HOL/IMP/Collecting_Examples.thy	Mon Jan 07 23:20:36 2013 +0100
+++ b/src/HOL/IMP/Collecting_Examples.thy	Tue Jan 08 10:34:19 2013 +0100
@@ -10,30 +10,30 @@
 text{* The example: *}
 definition "c = WHILE Less (V ''x'') (N 3)
                 DO ''x'' ::= Plus (V ''x'') (N 2)"
-definition c0 :: "state set acom" where "c0 = anno {} c"
+definition C0 :: "state set acom" where "C0 = anno {} c"
 
 definition "show_acom xs = map_acom (\<lambda>S. show_state xs ` S)"
 
 text{* Collecting semantics: *}
-value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 1) c0)"
-value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 2) c0)"
-value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 3) c0)"
-value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 4) c0)"
-value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 5) c0)"
-value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 6) c0)"
-value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 7) c0)"
-value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 8) c0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 1) C0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 2) C0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 3) C0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 4) C0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 5) C0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 6) C0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 7) C0)"
+value "show_acom [''x''] (((step {\<lambda>x. 0}) ^^ 8) C0)"
 
 text{* Small-step semantics: *}
-value "show_acom [''x''] (((step {}) ^^ 0) (step {\<lambda>x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 1) (step {\<lambda>x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 2) (step {\<lambda>x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 3) (step {\<lambda>x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 4) (step {\<lambda>x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 5) (step {\<lambda>x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 6) (step {\<lambda>x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 7) (step {\<lambda>x. 0} c0))"
-value "show_acom [''x''] (((step {}) ^^ 8) (step {\<lambda>x. 0} c0))"
+value "show_acom [''x''] (((step {}) ^^ 0) (step {\<lambda>x. 0} C0))"
+value "show_acom [''x''] (((step {}) ^^ 1) (step {\<lambda>x. 0} C0))"
+value "show_acom [''x''] (((step {}) ^^ 2) (step {\<lambda>x. 0} C0))"
+value "show_acom [''x''] (((step {}) ^^ 3) (step {\<lambda>x. 0} C0))"
+value "show_acom [''x''] (((step {}) ^^ 4) (step {\<lambda>x. 0} C0))"
+value "show_acom [''x''] (((step {}) ^^ 5) (step {\<lambda>x. 0} C0))"
+value "show_acom [''x''] (((step {}) ^^ 6) (step {\<lambda>x. 0} C0))"
+value "show_acom [''x''] (((step {}) ^^ 7) (step {\<lambda>x. 0} C0))"
+value "show_acom [''x''] (((step {}) ^^ 8) (step {\<lambda>x. 0} C0))"
 
 
 end