# HG changeset patch
# User wenzelm
# Date 1150138705 -7200
# Node ID e5c12b5cb9403cbca8125bb758649aee055be54b
# Parent  d319e39a2e0e2f047803311cf0deb144acee4692
avoid accidental binding of ?Jmp;

diff -r d319e39a2e0e -r e5c12b5cb940 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Mon Jun 12 20:32:33 2006 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Mon Jun 12 20:58:25 2006 +0200
@@ -275,12 +275,12 @@
      and wt: "Env\<turnstile>t\<Colon>T" 
      and wf: "wf_prog G"
      and  G: "prg Env = G"
-     and no_jmp: "\<forall> j. abrupt s0 = Some (Jump j) \<longrightarrow> j \<in> jmps"
+     and no_jmp: "\<forall>j. abrupt s0 = Some (Jump j) \<longrightarrow> j \<in> jmps"
                     (is "?Jmp jmps s0")
-  shows  "?Jmp jmps s1 \<and> 
+  shows  "(\<forall>j. fst s1 = Some (Jump j) \<longrightarrow> j \<in> jmps) \<and>
                  (normal s1 \<longrightarrow>
-                  (\<forall> w upd. v=In2 (w,upd)  
-                   \<longrightarrow>   (\<forall> s j val. 
+                  (\<forall> w upd. v=In2 (w,upd)
+                   \<longrightarrow>   (\<forall> s j val.
                           abrupt s \<noteq> Some (Jump j) \<longrightarrow>
                           abrupt (upd val s) \<noteq> Some (Jump j))))"
         (is "?Jmp jmps s1 \<and> ?Upd v s1")