src/HOL/MicroJava/BV/BVNoTypeError.thy

   length apTs = length fpTs \<and> is_class G C \<and>
   (\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and> 
   method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> G \<turnstile> X \<preceq> Class C)"
   (is "?app ST LT = ?P ST LT")
 proof
-  assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_def)
+  assume "?P ST LT" thus "?app ST LT" by (auto simp add: list_all2_iff)
 next  
   assume app: "?app ST LT"
   hence l: "length fpTs < length ST" by simp
   obtain xs ys where xs: "ST = xs @ ys" "length xs = length fpTs"
   proof -

   from l xs obtain X ST' where "ys = X#ST'" by (auto simp add: neq_Nil_conv)
   ultimately
   have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
   with app
   show "?P ST LT"
-    apply (clarsimp simp add: list_all2_def)
+    apply (clarsimp simp add: list_all2_iff)
     apply (intro exI conjI)
     apply auto
     done
 qed
 
 lemma approx_loc_len [simp]:
   "approx_loc G hp loc LT \<Longrightarrow> length loc = length LT"
-  by (simp add: approx_loc_def list_all2_def)
+  by (simp add: approx_loc_def list_all2_iff)
 
 lemma approx_stk_len [simp]:
   "approx_stk G hp stk ST \<Longrightarrow> length stk = length ST"
   by (simp add: approx_stk_def)
 

       have [simp]: "stk!length ps = x" by (simp add: nth_append)
       from stk' l ps
       have [simp]: "take (length ps) stk = aps" by simp
       from w ps
       have widen: "list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs ps"
-        by (simp add: list_all2_def) 
+        by (simp add: list_all2_iff) 
 
       from stk' l ps have "length ps < length stk" by simp
       moreover
       from wf x C 
       have x: "G,hp \<turnstile> x ::\<preceq> Class C" by (rule conf_widen)