src/HOL/Import/HOLLight/hollight.imp

   "ZIP" > "List.zip"
   "ZCONSTR" > "HOLLight.hollight.ZCONSTR"
   "ZBOT" > "HOLLight.hollight.ZBOT"
   "WF" > "Wellfounded.wfP"
   "UNIV" > "Orderings.top_class.top" :: "'a => bool"
-  "UNIONS" > "Complete_Lattice.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
+  "UNIONS" > "Complete_Lattices.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
   "UNION" > "Lattices.sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
   "UNCURRY" > "HOLLight.hollight.UNCURRY"
   "TL" > "List.tl"
   "T" > "HOL.True"
   "SURJ" > "HOLLight.hollight.SURJ"

   "LAST" > "List.last"
   "ITSET" > "HOLLight.hollight.ITSET"
   "ITLIST2" > "HOLLightList.fold2"
   "ITLIST" > "List.foldr"
   "ISO" > "HOLLight.hollight.ISO"
-  "INTERS" > "Complete_Lattice.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
+  "INTERS" > "Complete_Lattices.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
   "INTER" > "Lattices.inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
   "INSERT" > "Set.insert"
   "INR" > "Sum_Type.Inr"
   "INL" > "Sum_Type.Inl"
   "INJP" > "HOLLight.hollight.INJP"

   "UNION_IDEMPOT" > "Big_Operators.lattice_class.Sup_fin.idem"
   "UNION_EMPTY" > "HOLLight.hollight.UNION_EMPTY"
   "UNION_COMM" > "Lattices.lattice_class.inf_sup_aci_5"
   "UNION_ASSOC" > "Lattices.lattice_class.inf_sup_aci_6"
   "UNION_ACI" > "HOLLight.hollight.UNION_ACI"
-  "UNIONS_UNION" > "Complete_Lattice.Union_Un_distrib"
+  "UNIONS_UNION" > "Complete_Lattices.Union_Un_distrib"
   "UNIONS_SUBSET" > "HOLLight.hollight.UNIONS_SUBSET"
   "UNIONS_INTERS" > "HOLLight.hollight.UNIONS_INTERS"
-  "UNIONS_INSERT" > "Complete_Lattice.Union_insert"
+  "UNIONS_INSERT" > "Complete_Lattices.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"
+  "UNIONS_2" > "Complete_Lattices.Un_eq_Union"
+  "UNIONS_1" > "Complete_Lattices.complete_lattice_class.Sup_singleton"
+  "UNIONS_0" > "Complete_Lattices.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"
   "TYDEF_int" > "HOLLight.hollight.TYDEF_int"

   "SUB_ADD_LCANCEL" > "Nat.diff_cancel"
   "SUB_ADD" > "Nat.le_add_diff_inverse2"
   "SUB_0" > "HOLLight.hollight.SUB_0"
   "SUBSET_UNIV" > "Orderings.top_class.top_greatest"
   "SUBSET_UNION_ABSORPTION" > "Lattices.semilattice_sup_class.le_iff_sup"
-  "SUBSET_UNIONS" > "Complete_Lattice.Union_mono"
+  "SUBSET_UNIONS" > "Complete_Lattices.Union_mono"
   "SUBSET_UNION" > "HOLLight.hollight.SUBSET_UNION"
   "SUBSET_TRANS" > "Orderings.order_trans_rules_23"
   "SUBSET_RESTRICT" > "HOLLight.hollight.SUBSET_RESTRICT"
   "SUBSET_REFL" > "Inductive.basic_monos_1"
   "SUBSET_PSUBSET_TRANS" > "Orderings.order_le_less_trans"

   "ISO_USAGE" > "HOLLight.hollight.ISO_USAGE"
   "ISO_REFL" > "HOLLight.hollight.ISO_REFL"
   "ISO_FUN" > "HOLLight.hollight.ISO_FUN"
   "IN_UNIV" > "Set.UNIV_I"
   "IN_UNIONS" > "HOLLight.hollight.IN_UNIONS"
-  "IN_UNION" > "Complete_Lattice.mem_simps_3"
+  "IN_UNION" > "Complete_Lattices.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"
-  "IN_INSERT" > "Complete_Lattice.mem_simps_1"
+  "IN_INTER" > "Complete_Lattices.mem_simps_4"
+  "IN_INSERT" > "Complete_Lattices.mem_simps_1"
   "IN_IMAGE" > "HOLLight.hollight.IN_IMAGE"
   "IN_ELIM_THM" > "HOLLight.hollight.IN_ELIM_THM"
   "IN_ELIM_PAIR_THM" > "HOLLight.hollight.IN_ELIM_PAIR_THM"
   "IN_DISJOINT" > "HOLLight.hollight.IN_DISJOINT"
-  "IN_DIFF" > "Complete_Lattice.mem_simps_6"
+  "IN_DIFF" > "Complete_Lattices.mem_simps_6"
   "IN_DELETE_EQ" > "HOLLight.hollight.IN_DELETE_EQ"
   "IN_DELETE" > "HOLLight.hollight.IN_DELETE"
   "IN_CROSS" > "HOLLight.hollight.IN_CROSS"
   "INT_WOP" > "HOLLight.hollight.INT_WOP"
   "INT_POW" > "HOLLight.hollight.INT_POW"

   "INTER_EMPTY" > "HOLLight.hollight.INTER_EMPTY"
   "INTER_COMM" > "Lattices.lattice_class.inf_sup_aci_1"
   "INTER_ASSOC" > "Lattices.lattice_class.inf_sup_aci_2"
   "INTER_ACI" > "HOLLight.hollight.INTER_ACI"
   "INTERS_UNIONS" > "HOLLight.hollight.INTERS_UNIONS"
-  "INTERS_INSERT" > "Complete_Lattice.Inter_insert"
+  "INTERS_INSERT" > "Complete_Lattices.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"
+  "INTERS_2" > "Complete_Lattices.Int_eq_Inter"
+  "INTERS_1" > "Complete_Lattices.complete_lattice_class.Inf_singleton"
+  "INTERS_0" > "Complete_Lattices.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"
   "INSERT_INTER" > "Set.Int_insert_left"