Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Import/HOLLight/hollight.imp
changeset 44845 5e51075cbd97
parent 44633 8a2fd7418435
child 44860 56101fa00193 
--- a/src/HOL/Import/HOLLight/hollight.imp	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Sep 09 00:22:18 2011 +0200
@@ -267,7 +267,7 @@
   "WF" > "Wellfounded.wfP"
   "UNIV" > "Orderings.top_class.top" :: "'a => bool"
   "UNIONS" > "Complete_Lattice.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
-  "UNION" > "Lattices.semilattice_sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
+  "UNION" > "Lattices.sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
   "UNCURRY" > "HOLLight.hollight.UNCURRY"
   "TL" > "List.tl"
   "T" > "HOL.True"
@@ -317,7 +317,7 @@
   "ITLIST" > "List.foldr"
   "ISO" > "HOLLight.hollight.ISO"
   "INTERS" > "Complete_Lattice.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
-  "INTER" > "Lattices.semilattice_inf_class.inf" :: "('a => bool) => ('a => 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"
isabelle