--- 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