# HG changeset patch
# User nipkow
# Date 1369642431 -7200
# Node ID 785d39ee875397079a06baa0d616373ac40cd260
# Parent  31bd65d96f4d14e8909f3df03851d5122d0bd2e8
tuned

diff -r 31bd65d96f4d -r 785d39ee8753 src/HOL/IMP/Hoare_Sound_Complete.thy
--- a/src/HOL/IMP/Hoare_Sound_Complete.thy	Mon May 27 09:15:26 2013 +0200
+++ b/src/HOL/IMP/Hoare_Sound_Complete.thy	Mon May 27 10:13:51 2013 +0200
@@ -8,12 +8,12 @@
 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"
+    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(2) unfolding hoare_valid_def by blast
+        using While.IH unfolding hoare_valid_def by blast
     qed
   }
   thus ?case unfolding hoare_valid_def by blast