src/HOL/HOLCF/Library/HOL_Cpo.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 42151 4da4fc77664b
child 58880 0baae4311a9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents:
diff changeset
     5
header {* Cpo class instances for all HOL types *}
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