--- a/src/HOL/HOLCF/Discrete.thy Fri Nov 15 21:04:51 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-(* Title: HOL/HOLCF/Discrete.thy
- Author: Tobias Nipkow
-*)
-
-section \<open>Discrete cpo types\<close>
-
-theory Discrete
- imports Cont
-begin
-
-datatype 'a discr = Discr "'a :: type"
-
-subsection \<open>Discrete cpo class instance\<close>
-
-instantiation discr :: (type) discrete_cpo
-begin
-
-definition "((\<sqsubseteq>) :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (=)"
-
-instance
- by standard (simp add: below_discr_def)
-
-end
-
-
-subsection \<open>\emph{undiscr}\<close>
-
-definition undiscr :: "('a::type)discr \<Rightarrow> 'a"
- where "undiscr x = (case x of Discr y \<Rightarrow> y)"
-
-lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
- by (simp add: undiscr_def)
-
-lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
- by (induct y) simp
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Discrete_Cpo.thy Fri Nov 15 21:43:22 2024 +0100
@@ -0,0 +1,37 @@
+(* Title: HOL/HOLCF/Discrete_Cpo.thy
+ Author: Tobias Nipkow
+*)
+
+section \<open>Discrete cpo types\<close>
+
+theory Discrete_Cpo
+ imports Cont
+begin
+
+datatype 'a discr = Discr "'a :: type"
+
+subsection \<open>Discrete cpo class instance\<close>
+
+instantiation discr :: (type) discrete_cpo
+begin
+
+definition "((\<sqsubseteq>) :: 'a discr \<Rightarrow> 'a discr \<Rightarrow> bool) = (=)"
+
+instance
+ by standard (simp add: below_discr_def)
+
+end
+
+
+subsection \<open>\emph{undiscr}\<close>
+
+definition undiscr :: "('a::type)discr \<Rightarrow> 'a"
+ where "undiscr x = (case x of Discr y \<Rightarrow> y)"
+
+lemma undiscr_Discr [simp]: "undiscr (Discr x) = x"
+ by (simp add: undiscr_def)
+
+lemma Discr_undiscr [simp]: "Discr (undiscr y) = y"
+ by (induct y) simp
+
+end
--- a/src/HOL/HOLCF/Lift.thy Fri Nov 15 21:04:51 2024 +0100
+++ b/src/HOL/HOLCF/Lift.thy Fri Nov 15 21:43:22 2024 +0100
@@ -5,7 +5,7 @@
section \<open>Lifting types of class type to flat pcpo's\<close>
theory Lift
-imports Discrete Up
+imports Discrete_Cpo Up
begin
default_sort type