src/HOL/HOLCF/Lift.thy
changeset 81575 cb57350beaa9
parent 81446 cea55809bb9d
child 81577 a712bf5ccab0
--- a/src/HOL/HOLCF/Lift.thy	Tue Dec 10 22:40:07 2024 +0100
+++ b/src/HOL/HOLCF/Lift.thy	Tue Dec 10 22:59:13 2024 +0100
@@ -5,7 +5,7 @@
 section \<open>Lifting types of class type to flat pcpo's\<close>
 
 theory Lift
-imports Discrete_Cpo Up
+imports Up
 begin
 
 default_sort type