src/HOL/HOLCF/Library/HOL_Cpo.thy
author wenzelm
Sun Nov 02 17:16:01 2014 +0100 (2014-11-02)
changeset 58880 0baae4311a9f
parent 42151 4da4fc77664b
child 62175 8ffc4d0e652d
permissions -rw-r--r--
modernized header;
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/Library/HOL_Cpo.thy
huffman@41112
     2
    Author:     Brian Huffman
huffman@41112
     3
*)
huffman@41112
     4
wenzelm@58880
     5
section {* Cpo class instances for all HOL types *}
huffman@41112
     6
huffman@41112
     7
theory HOL_Cpo
huffman@41112
     8
imports
huffman@41112
     9
  Bool_Discrete
huffman@41112
    10
  Nat_Discrete
huffman@41112
    11
  Int_Discrete
huffman@41112
    12
  Char_Discrete
huffman@41112
    13
  Sum_Cpo
huffman@41112
    14
  Option_Cpo
huffman@41112
    15
  List_Predomain
huffman@41112
    16
begin
huffman@41112
    17
huffman@41112
    18
end