# HG changeset patch
# User wenzelm
# Date 1491335863 -7200
# Node ID ae93953746fca8872296ef5005a82906ace2c953
# Parent  76a96e32bd237a1ba82977fc4ee72bcacdc560fc
eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;

diff -r 76a96e32bd23 -r ae93953746fc src/HOL/HOLCF/Bifinite.thy
--- 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
diff -r 76a96e32bd23 -r ae93953746fc src/HOL/HOLCF/Completion.thy
--- 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>
diff -r 76a96e32bd23 -r ae93953746fc src/HOL/HOLCF/Deflation.thy
--- 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
diff -r 76a96e32bd23 -r ae93953746fc src/HOL/HOLCF/Fixrec.thy
--- 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
diff -r 76a96e32bd23 -r ae93953746fc src/HOL/HOLCF/Map_Functions.thy
--- 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>
diff -r 76a96e32bd23 -r ae93953746fc src/HOL/HOLCF/Plain_HOLCF.thy
--- 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
diff -r 76a96e32bd23 -r ae93953746fc src/HOL/ROOT
--- 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"