# HG changeset patch
# User nipkow
# Date 1510661568 -3600
# Node ID b5c1f0c76d3507111b2e81bafe2f2e523d15c54e
# Parent  f11486d3158630349ae9ef9b6e6221f4dabb2c58# Parent  a462583f0a37dde46b4364e9e10d93f1e29f264d
merged

diff -r f11486d31586 -r b5c1f0c76d35 src/HOL/IMP/Big_Step.thy
--- a/src/HOL/IMP/Big_Step.thy	Mon Nov 13 15:07:03 2017 +0100
+++ b/src/HOL/IMP/Big_Step.thy	Tue Nov 14 13:12:48 2017 +0100
@@ -206,13 +206,11 @@
       thus ?thesis using `\<not>bval b s` by blast
     next
       case IfTrue
-      with `(?iw, s) \<Rightarrow> t` have "(c;; ?w, s) \<Rightarrow> t" by auto
       -- "and for this, only the Seq-rule is applicable:"
-      then obtain s' where
+      from `(c;; ?w, s) \<Rightarrow> t` obtain s' where
         "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
-      -- "with this information, we can build a derivation tree for the @{text WHILE}"
-      with `bval b s`
-      show ?thesis by (rule WhileTrue)
+      -- "with this information, we can build a derivation tree for @{text WHILE}"
+      with `bval b s` show ?thesis by (rule WhileTrue)
     qed
   qed
   ultimately