# HG changeset patch
# User nipkow
# Date 1700141625 -3600
# Node ID c7db5b4dbaceb7d2d330dd9a5c80f29dbd76de05
# Parent  8da0eedd562c59d4fdc3e208120789b768e318bb
tuned

diff -r 8da0eedd562c -r c7db5b4dbace src/HOL/IMP/Big_Step.thy
--- 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