src/HOL/Bali/Evaln.thy
changeset 24727 dd9ea6b72eb9
parent 24165 605f664d5115
child 26480 544cef16045b
     1.1 --- a/src/HOL/Bali/Evaln.thy	Wed Sep 26 19:18:01 2007 +0200
     1.2 +++ b/src/HOL/Bali/Evaln.thy	Wed Sep 26 19:19:38 2007 +0200
     1.3 @@ -410,7 +410,7 @@
     1.4    shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
     1.5  using evaln 
     1.6  proof (induct)
     1.7 -  case (Loop s0 e n b s1 c s2 l s3)
     1.8 +  case (Loop s0 e b n s1 c s2 l s3)
     1.9    note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
    1.10    moreover
    1.11    have "if the_Bool b