eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
authorwenzelm
Tue Apr 04 21:57:43 2017 +0200 (2017-04-04)
changeset 65380ae93953746fc
parent 65379 76a96e32bd23
child 65381 9d9e6dac9690
eliminated Plain_HOLCF.thy (see also 8e92772bc0e8): it was modeled after HOL/Plain.thy which was discontinued later;
src/HOL/HOLCF/Bifinite.thy
src/HOL/HOLCF/Completion.thy
src/HOL/HOLCF/Deflation.thy
src/HOL/HOLCF/Fixrec.thy
src/HOL/HOLCF/Map_Functions.thy
src/HOL/HOLCF/Plain_HOLCF.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/HOLCF/Bifinite.thy	Tue Apr 04 21:45:54 2017 +0200
     1.2 +++ b/src/HOL/HOLCF/Bifinite.thy	Tue Apr 04 21:57:43 2017 +0200
     1.3 @@ -5,7 +5,7 @@
     1.4  section \<open>Profinite and bifinite cpos\<close>
     1.5  
     1.6  theory Bifinite
     1.7 -imports Map_Functions "~~/src/HOL/Library/Countable"
     1.8 +imports Map_Functions Cprod Sprod Sfun Up "~~/src/HOL/Library/Countable"
     1.9  begin
    1.10  
    1.11  default_sort cpo
     2.1 --- a/src/HOL/HOLCF/Completion.thy	Tue Apr 04 21:45:54 2017 +0200
     2.2 +++ b/src/HOL/HOLCF/Completion.thy	Tue Apr 04 21:57:43 2017 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4  section \<open>Defining algebraic domains by ideal completion\<close>
     2.5  
     2.6  theory Completion
     2.7 -imports Plain_HOLCF
     2.8 +imports Cfun
     2.9  begin
    2.10  
    2.11  subsection \<open>Ideals over a preorder\<close>
     3.1 --- a/src/HOL/HOLCF/Deflation.thy	Tue Apr 04 21:45:54 2017 +0200
     3.2 +++ b/src/HOL/HOLCF/Deflation.thy	Tue Apr 04 21:57:43 2017 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4  section \<open>Continuous deflations and ep-pairs\<close>
     3.5  
     3.6  theory Deflation
     3.7 -imports Plain_HOLCF
     3.8 +imports Cfun
     3.9  begin
    3.10  
    3.11  default_sort cpo
     4.1 --- a/src/HOL/HOLCF/Fixrec.thy	Tue Apr 04 21:45:54 2017 +0200
     4.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Tue Apr 04 21:57:43 2017 +0200
     4.3 @@ -5,7 +5,7 @@
     4.4  section "Package for defining recursive functions in HOLCF"
     4.5  
     4.6  theory Fixrec
     4.7 -imports Plain_HOLCF
     4.8 +imports Cprod Sprod Ssum Up One Tr Fix
     4.9  keywords "fixrec" :: thy_decl
    4.10  begin
    4.11  
    4.12 @@ -139,7 +139,7 @@
    4.13    match_TT :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
    4.14  where
    4.15    "match_TT = (\<Lambda> x k. If x then k else fail)"
    4.16 - 
    4.17 +
    4.18  definition
    4.19    match_FF :: "tr \<rightarrow> 'c match \<rightarrow> 'c match"
    4.20  where
     5.1 --- a/src/HOL/HOLCF/Map_Functions.thy	Tue Apr 04 21:45:54 2017 +0200
     5.2 +++ b/src/HOL/HOLCF/Map_Functions.thy	Tue Apr 04 21:57:43 2017 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4  section \<open>Map functions for various types\<close>
     5.5  
     5.6  theory Map_Functions
     5.7 -imports Deflation
     5.8 +imports Deflation Sprod Ssum Sfun Up
     5.9  begin
    5.10  
    5.11  subsection \<open>Map operator for continuous function space\<close>
     6.1 --- a/src/HOL/HOLCF/Plain_HOLCF.thy	Tue Apr 04 21:45:54 2017 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,15 +0,0 @@
     6.4 -(*  Title:      HOL/HOLCF/Plain_HOLCF.thy
     6.5 -    Author:     Brian Huffman
     6.6 -*)
     6.7 -
     6.8 -section \<open>Plain HOLCF\<close>
     6.9 -
    6.10 -theory Plain_HOLCF
    6.11 -imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
    6.12 -begin
    6.13 -
    6.14 -text \<open>
    6.15 -  Basic HOLCF concepts and types; does not include definition packages.
    6.16 -\<close>
    6.17 -
    6.18 -end
     7.1 --- a/src/HOL/ROOT	Tue Apr 04 21:45:54 2017 +0200
     7.2 +++ b/src/HOL/ROOT	Tue Apr 04 21:57:43 2017 +0200
     7.3 @@ -1039,7 +1039,6 @@
     7.4      "~~/src/HOL/Library/Nat_Bijection"
     7.5      "~~/src/HOL/Library/Countable"
     7.6    theories
     7.7 -    Plain_HOLCF
     7.8      Fixrec
     7.9      HOLCF
    7.10    document_files "root.tex"