1.1 --- a/src/HOL/IMP/Big_Step.thy	Fri Nov 10 22:05:30 2017 +0100
     1.2 +++ b/src/HOL/IMP/Big_Step.thy	Tue Nov 14 13:12:13 2017 +0100
     1.3 @@ -206,13 +206,11 @@
     1.4        thus ?thesis using `\<not>bval b s` by blast
     1.5      next
     1.6        case IfTrue
     1.7 -      with `(?iw, s) \<Rightarrow> t` have "(c;; ?w, s) \<Rightarrow> t" by auto
     1.8        -- "and for this, only the Seq-rule is applicable:"
     1.9 -      then obtain s' where
    1.10 +      from `(c;; ?w, s) \<Rightarrow> t` obtain s' where
    1.11          "(c, s) \<Rightarrow> s'" and "(?w, s') \<Rightarrow> t" by auto
    1.12 -      -- "with this information, we can build a derivation tree for the @{text WHILE}"
    1.13 -      with `bval b s`
    1.14 -      show ?thesis by (rule WhileTrue)
    1.15 +      -- "with this information, we can build a derivation tree for @{text WHILE}"
    1.16 +      with `bval b s` show ?thesis by (rule WhileTrue)
    1.17      qed
    1.18    qed
    1.19    ultimately