# HG changeset patch
# User nipkow
# Date 1731703046 -3600
# Node ID cea55809bb9d46a6cb9ffb8e3800d3afc64d7958
# Parent  82110cbcf9a1d0874cbceaa4a72a0aa01108a623
mv Discrete to Discrete_Cpo to avoid theory name clashes

diff -r 82110cbcf9a1 -r cea55809bb9d src/HOL/HOLCF/Discrete.thy
--- a/src/HOL/HOLCF/Discrete.thy	Thu Nov 14 11:33: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
diff -r 82110cbcf9a1 -r cea55809bb9d src/HOL/HOLCF/Discrete_Cpo.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/HOLCF/Discrete_Cpo.thy	Fri Nov 15 21:37:26 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
diff -r 82110cbcf9a1 -r cea55809bb9d src/HOL/HOLCF/Lift.thy
--- a/src/HOL/HOLCF/Lift.thy	Thu Nov 14 11:33:51 2024 +0100
+++ b/src/HOL/HOLCF/Lift.thy	Fri Nov 15 21:37:26 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