src/HOL/SMT.thy

 higher-order functions.  The following set of lemmas specifies the
 properties of such (extensional) arrays.
 *}
 
 lemmas array_rules = ext fun_upd_apply fun_upd_same fun_upd_other
-  fun_upd_upd
+  fun_upd_upd fun_app_def
 
 
 
 subsection {* First-order logic *}