--- a/src/HOL/Import/offline/maps.lst Mon Jan 20 23:30:06 2025 +0100
+++ b/src/HOL/Import/offline/maps.lst Mon Jan 20 13:03:50 2025 +0100
@@ -36,6 +36,8 @@
num_Axiom num_Axiom
DEF_BIT0
DEF_BIT1
+DEF_WF -
+WF WF
DEF_PRE -
PRE PRE
DEF_+ -
@@ -81,23 +83,12 @@
TL TL
DEF_APPEND -
APPEND APPEND
-DEF_REVERSE -
DEF_LENGTH -
LENGTH LENGTH
DEF_MAP -
MAP MAP
DEF_LAST -
LAST LAST
-DEF_BUTLAST -
-DEF_REPLICATE -
-DEF_NULL -
-DEF_ALL -
-DEF_EX -
-DEF_ITLIST -
-DEF_ALL2 -
-DEF_FILTER -
-DEF_ZIP -
-ZIP_DEF -
TYDEF_real -
DEF_real_of_num -
real_of_num -