src/HOL/Bali/TypeSafe.thy
changeset 23373 ead82c82da9e
parent 23350 50c5b0912a0c
child 24019 67bde7cfcf10
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Wed Jun 13 16:43:02 2007 +0200
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Wed Jun 13 18:30:11 2007 +0200
     1.3 @@ -2680,8 +2680,8 @@
     1.4      qed
     1.5    next
     1.6      case (Super s L accC T A)
     1.7 -    have conf_s: "Norm s\<Colon>\<preceq>(G, L)" .
     1.8 -    have     wt: "\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T" .
     1.9 +    note conf_s = `Norm s\<Colon>\<preceq>(G, L)`
    1.10 +    note wt = `\<lparr>prg = G, cls = accC, lcl = L\<rparr>\<turnstile>In1l Super\<Colon>T`
    1.11      then obtain C c where
    1.12               C: "L This = Some (Class C)" and
    1.13         neq_Obj: "C\<noteq>Object" and
    1.14 @@ -3426,10 +3426,10 @@
    1.15        have "\<And> j. abrupt s2 = Some (Jump j) \<Longrightarrow> j=Ret"
    1.16  	by (rule jumpNestingOk_evalE) (auto intro: jmpOk simp add: s1_no_jmp)
    1.17        moreover 
    1.18 -      have "s3 =
    1.19 +      note `s3 =
    1.20                  (if \<exists>l. abrupt s2 = Some (Jump (Break l)) \<or> 
    1.21                          abrupt s2 = Some (Jump (Cont l))
    1.22 -                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)" .
    1.23 +                 then abupd (\<lambda>x. Some (Error CrossMethodJump)) s2 else s2)`
    1.24        ultimately show ?thesis
    1.25  	by force
    1.26      qed
    1.27 @@ -3649,8 +3649,8 @@
    1.28  	from eval_e1 wt_e1 da_e1 wf True
    1.29  	have "nrm E1 \<subseteq> dom (locals (store s1))"
    1.30  	  by (cases rule: da_good_approxE') iprover
    1.31 -	with da_e2 show ?thesis
    1.32 -	  by (rule da_weakenE)
    1.33 +	with da_e2 show thesis
    1.34 +	  by (rule da_weakenE) (rule that)
    1.35        qed
    1.36        with conf_s1 wt_e2
    1.37        obtain conf_s2: "s2\<Colon>\<preceq>(G, L)" and error_free_s2: "error_free s2"