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