src/HOL/Import/HOLLight/hollight.imp

   "UNIONS_SUBSET" > "HOLLight.hollight.UNIONS_SUBSET"
   "UNIONS_INTERS" > "HOLLight.hollight.UNIONS_INTERS"
   "UNIONS_INSERT" > "Complete_Lattice.Union_insert"
   "UNIONS_IMAGE" > "HOLLight.hollight.UNIONS_IMAGE"
   "UNIONS_GSPEC" > "HOLLight.hollight.UNIONS_GSPEC"
+  "UNIONS_2" > "Complete_Lattice.Un_eq_Union"
+  "UNIONS_1" > "Complete_Lattice.complete_lattice_class.Sup_singleton"
   "UNIONS_0" > "Complete_Lattice.Union_empty"
   "UNCURRY_def" > "HOLLight.hollight.UNCURRY_def"
   "TYDEF_recspace" > "HOLLight.hollight.TYDEF_recspace"
   "TYDEF_real" > "HOLLight.hollight.TYDEF_real"
   "TYDEF_nadd" > "HOLLight.hollight.TYDEF_nadd"

   "INTER_ACI" > "HOLLight.hollight.INTER_ACI"
   "INTERS_UNIONS" > "HOLLight.hollight.INTERS_UNIONS"
   "INTERS_INSERT" > "Complete_Lattice.Inter_insert"
   "INTERS_IMAGE" > "HOLLight.hollight.INTERS_IMAGE"
   "INTERS_GSPEC" > "HOLLight.hollight.INTERS_GSPEC"
+  "INTERS_2" > "Complete_Lattice.Int_eq_Inter"
+  "INTERS_1" > "Complete_Lattice.complete_lattice_class.Inf_singleton"
   "INTERS_0" > "Complete_Lattice.Inter_empty"
   "INSERT_UNIV" > "HOLLight.hollight.INSERT_UNIV"
   "INSERT_UNION_EQ" > "Set.Un_insert_left"
   "INSERT_UNION" > "HOLLight.hollight.INSERT_UNION"
   "INSERT_SUBSET" > "Set.insert_subset"

   "HAS_SIZE_CARD" > "HOLLight.hollight.HAS_SIZE_CARD"
   "HAS_SIZE_1" > "HOLLight.hollight.HAS_SIZE_1"
   "HAS_SIZE_0" > "HOLLight.hollight.HAS_SIZE_0"
   "GE_C" > "HOLLight.hollight.GE_C"
   "FUN_IN_IMAGE" > "Set.imageI"
-  "FUN_EQ_THM" > "Fun.fun_eq_iff"
+  "FUN_EQ_THM" > "HOL.fun_eq_iff"
   "FUNCTION_FACTORS_RIGHT" > "HOLLight.hollight.FUNCTION_FACTORS_RIGHT"
   "FUNCTION_FACTORS_LEFT" > "HOLLight.hollight.FUNCTION_FACTORS_LEFT"
   "FST" > "Product_Type.fst_conv"
   "FORALL_UNWIND_THM2" > "HOL.simp_thms_41"
   "FORALL_UNWIND_THM1" > "HOL.simp_thms_42"

   "DEF__greaterthan_" > "HOLLightCompat.DEF__greaterthan_"
   "DEF__exclamationmark_" > "HOL.All_def"
   "DEF__equal__equal__greaterthan_" > "HOLLightCompat.DEF__equal__equal__greaterthan_"
   "DEF__equal__equal_" > "HOLLight.hollight.DEF__equal__equal_"
   "DEF__equal__c" > "HOLLight.hollight.DEF__equal__c"
-  "DEF__dot__dot_" > "HOLLightCompat.DEF__dot__dot_"
+  "DEF__dot__dot_" > "HOLLightCompat.dotdot_def"
   "DEF__backslash__slash_" > "HOL.or_def"
   "DEF__UNGUARDED_PATTERN" > "HOLLight.hollight.DEF__UNGUARDED_PATTERN"
   "DEF__SEQPATTERN" > "HOLLight.hollight.DEF__SEQPATTERN"
   "DEF__MATCH" > "HOLLight.hollight.DEF__MATCH"
   "DEF__GUARDED_PATTERN" > "HOLLight.hollight.DEF__GUARDED_PATTERN"

   "DEF_IND_0" > "HOLLight.hollight.DEF_IND_0"
   "DEF_IN" > "Set.mem_def"
   "DEF_IMAGE" > "HOLLightCompat.DEF_IMAGE"
   "DEF_I" > "Fun.id_apply"
   "DEF_HAS_SIZE" > "HOLLight.hollight.DEF_HAS_SIZE"
-  "DEF_GSPEC" > "HOLLightCompat.DEF_GSPEC"
+  "DEF_GSPEC" > "Set.Collect_def"
   "DEF_GEQ" > "HOLLightCompat.DEF_GEQ"
   "DEF_GABS" > "HOLLightCompat.DEF_GABS"
   "DEF_FST" > "HOLLightCompat.DEF_FST"
   "DEF_FNIL" > "HOLLight.hollight.DEF_FNIL"
   "DEF_FINREC" > "HOLLight.hollight.DEF_FINREC"