src/HOL/Import/HOLLight/hollight.imp
changeset 44845 5e51075cbd97
parent 44633 8a2fd7418435
child 44860 56101fa00193
     1.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Thu Sep 08 08:41:28 2011 -0700
     1.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Sep 09 00:22:18 2011 +0200
     1.3 @@ -267,7 +267,7 @@
     1.4    "WF" > "Wellfounded.wfP"
     1.5    "UNIV" > "Orderings.top_class.top" :: "'a => bool"
     1.6    "UNIONS" > "Complete_Lattice.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
     1.7 -  "UNION" > "Lattices.semilattice_sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
     1.8 +  "UNION" > "Lattices.sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
     1.9    "UNCURRY" > "HOLLight.hollight.UNCURRY"
    1.10    "TL" > "List.tl"
    1.11    "T" > "HOL.True"
    1.12 @@ -317,7 +317,7 @@
    1.13    "ITLIST" > "List.foldr"
    1.14    "ISO" > "HOLLight.hollight.ISO"
    1.15    "INTERS" > "Complete_Lattice.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
    1.16 -  "INTER" > "Lattices.semilattice_inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
    1.17 +  "INTER" > "Lattices.inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
    1.18    "INSERT" > "Set.insert"
    1.19    "INR" > "Sum_Type.Inr"
    1.20    "INL" > "Sum_Type.Inl"