src/HOL/Import/HOLLight/hollight.imp
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 43786 fea3ed6951e3
--- a/src/HOL/Import/HOLLight/hollight.imp	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp	Mon Sep 13 11:13:15 2010 +0200
@@ -1394,7 +1394,7 @@
   "GSPEC_def" > "HOLLight.hollight.GSPEC_def"
   "GEQ_def" > "HOLLight.hollight.GEQ_def"
   "GABS_def" > "HOLLight.hollight.GABS_def"
-  "FUN_EQ_THM" > "Fun.ext_iff"
+  "FUN_EQ_THM" > "Fun.fun_eq_iff"
   "FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
   "FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
   "FSTCART_PASTECART" > "HOLLight.hollight.FSTCART_PASTECART"