src/HOL/MicroJava/BV/BVSpecTypeSafe.thy

     with cr' match phi' meth  
     show ?thesis by (unfold correct_state_def) auto
   qed
 qed
 
-
+declare raise_if_def [simp]
 text {*
   The requirement of lemma @{text uncaught_xcpt_correct} (that
   the exception is a valid reference on the heap) is always met
   for welltyped instructions and conformant states:
 *}