src/HOL/IMP/Natural.thy

     -- "both cases together give us what we want:"
     have "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'" by blast
   }
   moreover
   -- "now the other direction:"
-  { fix s s' assume if: "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
+  { fix s s' assume "if": "\<langle>?if, s\<rangle> \<longrightarrow>\<^sub>c s'"
     -- "again, if @{text b} is @{text False} in state @{text s}, then the False-branch"
     -- "of the @{text \<IF>} is executed, and both statements do nothing:"
     hence "\<not>b s \<Longrightarrow> s = s'" by simp
     hence "\<not>b s \<Longrightarrow> \<langle>?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by simp
     moreover
     -- "on the other hand, if @{text b} is @{text True} in state @{text s},"
     -- {* then this time only the @{text IfTrue} rule can have be used *}
     { assume b: "b s"
-      with if have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
+      with "if" have "\<langle>c; ?w, s\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
       -- "and for this, only the Semi-rule is applicable:"
       then obtain s'' where
         "\<langle>c, s\<rangle> \<longrightarrow>\<^sub>c s''" and "\<langle>?w, s''\<rangle> \<longrightarrow>\<^sub>c s'" by (cases set: evalc) auto
       -- "with this information, we can build a derivation tree for the @{text \<WHILE>}"
       with b