adapted variable order for inductive cases (determined by read_specification *before* expanding abbreviations);
authorwenzelm
Wed Sep 26 19:19:38 2007 +0200 (2007-09-26)
changeset 24727dd9ea6b72eb9
parent 24726 fcf13a91cda2
child 24728 e2b3a1065676
adapted variable order for inductive cases (determined by read_specification *before* expanding abbreviations);
src/HOL/Bali/AxSound.thy
src/HOL/Bali/Evaln.thy
     1.1 --- a/src/HOL/Bali/AxSound.thy	Wed Sep 26 19:18:01 2007 +0200
     1.2 +++ b/src/HOL/Bali/AxSound.thy	Wed Sep 26 19:19:38 2007 +0200
     1.3 @@ -2017,7 +2017,7 @@
     1.4                  \<rbrakk>\<Longrightarrow> (P'\<leftarrow>=False\<down>=\<diamondsuit>) v s' Z"
     1.5  	  (is "PROP ?Hyp n t s v s'")
     1.6  	proof (induct)
     1.7 -	  case (Loop s0' e' n' b s1' c' s2' l' s3' Y' T E)
     1.8 +	  case (Loop s0' e' b n' s1' c' s2' l' s3' Y' T E)
     1.9  	  note while = `(\<langle>l'\<bullet> While(e') c'\<rangle>\<^sub>s::term) = \<langle>l\<bullet> While(e) c\<rangle>\<^sub>s`
    1.10            hence eqs: "l'=l" "e'=e" "c'=c" by simp_all
    1.11  	  note valid_A = `\<forall>t\<in>A. G\<Turnstile>n'\<Colon>t`
     2.1 --- a/src/HOL/Bali/Evaln.thy	Wed Sep 26 19:18:01 2007 +0200
     2.2 +++ b/src/HOL/Bali/Evaln.thy	Wed Sep 26 19:19:38 2007 +0200
     2.3 @@ -410,7 +410,7 @@
     2.4    shows "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)"
     2.5  using evaln 
     2.6  proof (induct)
     2.7 -  case (Loop s0 e n b s1 c s2 l s3)
     2.8 +  case (Loop s0 e b n s1 c s2 l s3)
     2.9    note `G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1`
    2.10    moreover
    2.11    have "if the_Bool b