eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
--- a/src/HOL/HOLCF/Bifinite.thy Tue Apr 04 21:45:54 2017 +0200
+++ b/src/HOL/HOLCF/Bifinite.thy Tue Apr 04 21:57:43 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Profinite and bifinite cpos\<close>
theory Bifinite
-imports Map_Functions "~~/src/HOL/Library/Countable"
+imports Map_Functions Cprod Sprod Sfun Up "~~/src/HOL/Library/Countable"
begin
default_sort cpo
--- a/src/HOL/HOLCF/Completion.thy Tue Apr 04 21:45:54 2017 +0200
+++ b/src/HOL/HOLCF/Completion.thy Tue Apr 04 21:57:43 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Defining algebraic domains by ideal completion\<close>
theory Completion
-imports Plain_HOLCF
+imports Cfun
begin
subsection \<open>Ideals over a preorder\<close>
--- a/src/HOL/HOLCF/Deflation.thy Tue Apr 04 21:45:54 2017 +0200
+++ b/src/HOL/HOLCF/Deflation.thy Tue Apr 04 21:57:43 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Continuous deflations and ep-pairs\<close>
theory Deflation
-imports Plain_HOLCF
+imports Cfun
begin
default_sort cpo
--- a/src/HOL/HOLCF/Fixrec.thy Tue Apr 04 21:45:54 2017 +0200
+++ b/src/HOL/HOLCF/Fixrec.thy Tue Apr 04 21:57:43 2017 +0200
@@ -5,7 +5,7 @@
section "Package for defining recursive functions in HOLCF"
theory Fixrec
-imports Plain_HOLCF
+imports Cprod Sprod Ssum Up One Tr Fix
keywords "fixrec" :: thy_decl
begin
@@ -139,7 +139,7 @@
match_TT :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
where
"match_TT = (\<Lambda> x k. If x then k else fail)"
-
+
definition
match_FF :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
where
--- a/src/HOL/HOLCF/Map_Functions.thy Tue Apr 04 21:45:54 2017 +0200
+++ b/src/HOL/HOLCF/Map_Functions.thy Tue Apr 04 21:57:43 2017 +0200
@@ -5,7 +5,7 @@
section \<open>Map functions for various types\<close>
theory Map_Functions
-imports Deflation
+imports Deflation Sprod Ssum Sfun Up
begin
subsection \<open>Map operator for continuous function space\<close>
--- a/src/HOL/HOLCF/Plain_HOLCF.thy Tue Apr 04 21:45:54 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,15 +0,0 @@
-(* Title: HOL/HOLCF/Plain_HOLCF.thy
- Author: Brian Huffman
-*)
-
-section \<open>Plain HOLCF\<close>
-
-theory Plain_HOLCF
-imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
-begin
-
-text \<open>
- Basic HOLCF concepts and types; does not include definition packages.
-\<close>
-
-end
--- a/src/HOL/ROOT Tue Apr 04 21:45:54 2017 +0200
+++ b/src/HOL/ROOT Tue Apr 04 21:57:43 2017 +0200
@@ -1039,7 +1039,6 @@
"~~/src/HOL/Library/Nat_Bijection"
"~~/src/HOL/Library/Countable"
theories
- Plain_HOLCF
Fixrec
HOLCF
document_files "root.tex"