src/HOL/Bali/Evaln.thy
changeset 26932 c398a3866082
parent 26480 544cef16045b
child 27226 5a3e5e46d977
     1.1 --- a/src/HOL/Bali/Evaln.thy	Sat May 17 15:31:42 2008 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Sat May 17 21:46:22 2008 +0200
     1.3 @@ -582,7 +582,7 @@
     1.4    then show ?case ..
     1.5  next
     1.6    case (Jmp s j)
     1.7 -  have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
     1.8 +  fix n have "G\<turnstile>Norm s \<midarrow>Jmp j\<midarrow>n\<rightarrow> (Some (Jump j), s)"
     1.9      by (rule evaln.Jmp)
    1.10    then show ?case ..
    1.11  next
    1.12 @@ -681,7 +681,7 @@
    1.13    then show ?case ..
    1.14  next
    1.15    case (Lit s v)
    1.16 -  have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
    1.17 +  fix n have "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
    1.18      by (rule evaln.Lit)
    1.19    then show ?case ..
    1.20  next
    1.21 @@ -705,7 +705,7 @@
    1.22    then show ?case ..
    1.23  next
    1.24    case (Super s )
    1.25 -  have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
    1.26 +  fix n have "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
    1.27      by (rule evaln.Super)
    1.28    then show ?case ..
    1.29  next
    1.30 @@ -830,5 +830,5 @@
    1.31      by (blast intro!: evaln.Cons dest: evaln_max2)
    1.32    then show ?case ..
    1.33  qed
    1.34 -       
    1.35 +
    1.36  end