# HG changeset patch
# User nipkow
# Date 1360742687 -3600
# Node ID 3775bf0ea5b884f4c02459a6d7ec0b6e5e92006b
# Parent  73ddb9e6f6e8c17c06d045baa736fc055aef91dd
tuned names

diff -r 73ddb9e6f6e8 -r 3775bf0ea5b8 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Tue Feb 12 21:35:40 2013 +0100
+++ b/src/HOL/IMP/Collecting.thy	Wed Feb 13 09:04:47 2013 +0100
@@ -142,14 +142,14 @@
 subsubsection "Collecting semantics"
 
 fun step :: "state set \<Rightarrow> state set acom \<Rightarrow> state set acom" where
-"step S (SKIP {P}) = (SKIP {S})" |
-"step S (x ::= e {P}) =
+"step S (SKIP {Q}) = (SKIP {S})" |
+"step S (x ::= e {Q}) =
   x ::= e {{s(x := aval e s) |s. s : S}}" |
 "step S (C1; C2) = step S C1; step (post C1) C2" |
-"step S (IF b THEN {P1} C1 ELSE {P2} C2 {P}) =
+"step S (IF b THEN {P1} C1 ELSE {P2} C2 {Q}) =
   IF b THEN {{s:S. bval b s}} step P1 C1 ELSE {{s:S. \<not> bval b s}} step P2 C2
   {post C1 \<union> post C2}" |
-"step S ({I} WHILE b DO {P} C {P'}) =
+"step S ({I} WHILE b DO {P} C {Q}) =
   {S \<union> post C} WHILE b DO {{s:I. bval b s}} step P C {{s:I. \<not> bval b s}}"
 
 definition CS :: "com \<Rightarrow> state set acom" where