# HG changeset patch
# User nipkow
# Date 1323120583 -3600
# Node ID 5d35cb2c0f02f7edc160021d7c8409d8f04e7201
# Parent  2d5b1af2426a32133cdc3e8f025835efe356cc1d
tuned proof

diff -r 2d5b1af2426a -r 5d35cb2c0f02 src/HOL/IMP/Live.thy
--- a/src/HOL/IMP/Live.thy	Mon Dec 05 17:33:57 2011 +0100
+++ b/src/HOL/IMP/Live.thy	Mon Dec 05 22:29:43 2011 +0100
@@ -75,11 +75,11 @@
 next
   case (WhileFalse b s c)
   hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
-  thus ?case using WhileFalse(2) by auto
+  thus ?case using WhileFalse.prems by auto
 next
   case (WhileTrue b s1 c s2 s3 X t1)
   let ?w = "WHILE b DO c"
-  from `bval b s1` WhileTrue(6) have "bval b t1"
+  from `bval b s1` WhileTrue.prems have "bval b t1"
     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   have "s1 = t1 on L c (L ?w X)" using  L_While_subset WhileTrue.prems
     by (blast)
@@ -139,11 +139,11 @@
 next
   case (WhileFalse b s c)
   hence "~ bval b t" by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
-  thus ?case using WhileFalse(2) by auto
+  thus ?case using WhileFalse.prems by auto
 next
   case (WhileTrue b s1 c s2 s3 X t1)
   let ?w = "WHILE b DO c"
-  from `bval b s1` WhileTrue(6) have "bval b t1"
+  from `bval b s1` WhileTrue.prems have "bval b t1"
     by (auto simp: ball_Un) (metis bval_eq_if_eq_on_vars)
   have "s1 = t1 on L c (L ?w X)"
     using L_While_subset WhileTrue.prems by blast