summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 04 Apr 2017 21:57:43 +0200 | |

changeset 65380 | ae93953746fc |

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 | file | annotate | diff | comparison | revisions | |

src/HOL/HOLCF/Completion.thy | file | annotate | diff | comparison | revisions | |

src/HOL/HOLCF/Deflation.thy | file | annotate | diff | comparison | revisions | |

src/HOL/HOLCF/Fixrec.thy | file | annotate | diff | comparison | revisions | |

src/HOL/HOLCF/Map_Functions.thy | file | annotate | diff | comparison | revisions | |

src/HOL/HOLCF/Plain_HOLCF.thy | file | annotate | diff | comparison | revisions | |

src/HOL/ROOT | file | annotate | diff | comparison | revisions |

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