tuned

--- a/src/HOL/IMP/Big_Step.thy	Mon Nov 13 18:08:05 2023 +0100
+++ b/src/HOL/IMP/Big_Step.thy	Thu Nov 16 14:33:45 2023 +0100
@@ -202,7 +202,7 @@
     from assm show ?thesis
     proof cases \<comment> \<open>rule inversion on \<open>(?iw, s) \<Rightarrow> t\<close>\<close>
       case IfFalse
-      hence "s = t" using \<open>(?iw, s) \<Rightarrow> t\<close> by blast
+      hence "s = t" by blast
       thus ?thesis using \<open>\<not>bval b s\<close> by blast
     next
       case IfTrue