src/HOL/HOLCF/Library/HOL_Cpo.thy
author immler
Sun, 27 Oct 2019 21:51:14 -0400
changeset 71035 6fe5a0e1fa8e
parent 62175 8ffc4d0e652d
permissions -rw-r--r--
moved theory Interval from the AFP
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41112
diff changeset
     1
(*  Title:      HOL/HOLCF/Library/HOL_Cpo.thy
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     3
*)
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     4
62175
8ffc4d0e652d isabelle update_cartouches -c -t;
wenzelm
parents: 58880
diff changeset
     5
section \<open>Cpo class instances for all HOL types\<close>
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     6
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     7
theory HOL_Cpo
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     8
imports
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     9
  Bool_Discrete
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    10
  Nat_Discrete
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    11
  Int_Discrete
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    12
  Char_Discrete
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    13
  Sum_Cpo
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    14
  Option_Cpo
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    15
  List_Predomain
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    16
begin
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    17
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
    18
end