src/HOL/IMP/Sem_Equiv.thy
changeset 45200 1f1897ac7877
parent 45015 fdac1e9880eb
child 45218 f115540543d8
     1.1 --- a/src/HOL/IMP/Sem_Equiv.thy	Wed Oct 19 09:11:21 2011 +0200
     1.2 +++ b/src/HOL/IMP/Sem_Equiv.thy	Wed Oct 19 16:32:12 2011 +0200
     1.3 @@ -152,11 +152,11 @@
     1.4    "(\<And>s. P s \<Longrightarrow> \<not> bval b s) \<Longrightarrow> P \<Turnstile> WHILE b DO c \<sim> SKIP"
     1.5    by (auto simp: equiv_up_to_def)
     1.6  
     1.7 -lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (B True) DO c'"
     1.8 +lemma while_never: "(c, s) \<Rightarrow> u \<Longrightarrow> c \<noteq> WHILE (Bc True) DO c'"
     1.9   by (induct rule: big_step_induct) auto
    1.10    
    1.11  lemma equiv_up_to_while_True [intro!,simp]:
    1.12 -  "P \<Turnstile> WHILE B True DO c \<sim> WHILE B True DO SKIP"
    1.13 +  "P \<Turnstile> WHILE Bc True DO c \<sim> WHILE Bc True DO SKIP"
    1.14    unfolding equiv_up_to_def
    1.15    by (blast dest: while_never)
    1.16