src/HOL/IMP/Hoare_Sound_Complete.thy

--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Tue Nov 07 14:52:27 2017 +0100
@@ -11,15 +11,13 @@
 lemma hoare_sound: "\<turnstile> {P}c{Q}  \<Longrightarrow>  \<Turnstile> {P}c{Q}"
 proof(induction rule: hoare.induct)
   case (While P b c)
-  { fix s t
-    have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s  \<Longrightarrow>  P t \<and> \<not> bval b t"
-    proof(induction "WHILE b DO c" s t rule: big_step_induct)
-      case WhileFalse thus ?case by blast
-    next
-      case WhileTrue thus ?case
-        using While.IH unfolding hoare_valid_def by blast
-    qed
-  }
+  have "(WHILE b DO c,s) \<Rightarrow> t  \<Longrightarrow>  P s  \<Longrightarrow>  P t \<and> \<not> bval b t" for s t
+  proof(induction "WHILE b DO c" s t rule: big_step_induct)
+    case WhileFalse thus ?case by blast
+  next
+    case WhileTrue thus ?case
+      using While.IH unfolding hoare_valid_def by blast
+  qed
   thus ?case unfolding hoare_valid_def by blast
 qed (auto simp: hoare_valid_def)