src/HOL/Import/HOLLight/hollight.imp

   "WF_EREC" > "HOLLight.hollight.WF_EREC"
   "WF_EQ" > "HOLLight.hollight.WF_EQ"
   "WF_DCHAIN" > "HOLLight.hollight.WF_DCHAIN"
   "UNWIND_THM2" > "HOL.simp_thms_39"
   "UNWIND_THM1" > "HOL.simp_thms_40"
-  "UNIV_SUBSET" > "HOLLight.hollight.UNIV_SUBSET"
+  "UNIV_SUBSET" > "Orderings.top_class.top_unique"
   "UNIV_NOT_EMPTY" > "Set.UNIV_not_empty"
   "UNIQUE_SKOLEM_THM" > "HOL.choice_eq"
   "UNIQUE_SKOLEM_ALT" > "HOLLight.hollight.UNIQUE_SKOLEM_ALT"
   "UNION_UNIV" > "HOLLight.hollight.UNION_UNIV"
   "UNION_SUBSET" > "Lattices.semilattice_sup_class.le_sup_iff"

   "SUBSET_INTER_ABSORPTION" > "Lattices.semilattice_inf_class.le_iff_inf"
   "SUBSET_INTER" > "Lattices.semilattice_inf_class.le_inf_iff"
   "SUBSET_INSERT_DELETE" > "HOLLight.hollight.SUBSET_INSERT_DELETE"
   "SUBSET_INSERT" > "Set.subset_insert"
   "SUBSET_IMAGE" > "Set.subset_image_iff"
-  "SUBSET_EMPTY" > "Set.subset_empty"
+  "SUBSET_EMPTY" > "Orderings.bot_class.bot_unique"
   "SUBSET_DIFF" > "Set.Diff_subset"
   "SUBSET_DELETE" > "HOLLight.hollight.SUBSET_DELETE"
   "SUBSET_CARD_EQ" > "HOLLight.hollight.SUBSET_CARD_EQ"
   "SUBSET_ANTISYM_EQ" > "Orderings.order_class.eq_iff"
   "SUBSET_ANTISYM" > "Orderings.order_antisym"

   "IN_UNIV" > "Set.UNIV_I"
   "IN_UNIONS" > "HOLLight.hollight.IN_UNIONS"
   "IN_UNION" > "Complete_Lattice.mem_simps_3"
   "IN_SUPPORT" > "HOLLight.hollight.IN_SUPPORT"
   "IN_SING" > "Set.singleton_iff"
+  "IN_SET_OF_LIST" > "HOLLightList.IN_SET_OF_LIST"
   "IN_REST" > "HOLLight.hollight.IN_REST"
   "IN_NUMSEG_0" > "HOLLight.hollight.IN_NUMSEG_0"
   "IN_NUMSEG" > "SetInterval.ord_class.atLeastAtMost_iff"
   "IN_INTERS" > "HOLLight.hollight.IN_INTERS"
   "IN_INTER" > "Complete_Lattice.mem_simps_4"

   "<_c_def" > "HOLLight.hollight.<_c_def"
   "<=_c_def" > "HOLLight.hollight.<=_c_def"
   "$_def" > "HOLLight.hollight.$_def"
 
 ignore_thms
+  "WF_REC_CASES"
   "TYDEF_sum"
   "TYDEF_prod"
   "TYDEF_option"
   "TYDEF_num"
   "TYDEF_list"
   "TYDEF_1"
   "SNDCART_PASTECART"
   "SET_OF_LIST_OF_SET"
   "REP_ABS_PAIR"
+  "RECURSION_CASEWISE_PAIRWISE"
+  "RECURSION_CASEWISE"
   "PASTECART_FST_SND"
   "PASTECART_EQ"
   "MEM_LIST_OF_SET"
   "MEM_ASSOC"
   "LIST_OF_SET_PROPERTIES"
   "LENGTH_LIST_OF_SET"
+  "HAS_SIZE_SET_OF_LIST"
   "FSTCART_PASTECART"
   "FORALL_PASTECART"
   "FINITE_SET_OF_LIST"
   "EX_MAP"
   "EXISTS_PASTECART"

   "DEF_INL"
   "DEF_HD"
   "DEF_CONS"
   "DEF_ASSOC"
   "DEF_,"
+  "CASEWISE_WORKS"
+  "CASEWISE_CASES"
+  "CASEWISE"
+  "CARD_SET_OF_LIST_LE"
   "ALL_MAP"
 
 end