src/HOL/HOLCF/Library/HOLCF_Library.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 41112 866148b76247
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:
37110
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff changeset
     1
theory HOLCF_Library
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff changeset
     2
imports
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents: 40774
diff changeset
     3
  Bool_Discrete
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents: 40774
diff changeset
     4
  Char_Discrete
39999
e3948547b541 add HOLCF/Library/Defl_Bifinite.thy, which proves instance defl :: bifinite
huffman
parents: 39143
diff changeset
     5
  Defl_Bifinite
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents: 40774
diff changeset
     6
  Int_Discrete
39143
d80990d8b909 add List_Cpo.thy to HOLCF/Library
huffman
parents: 37111
diff changeset
     7
  List_Cpo
41112
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents: 40774
diff changeset
     8
  List_Predomain
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents: 40774
diff changeset
     9
  Nat_Discrete
866148b76247 add HOLCF library theories with cpo/predomain instances for HOL types
huffman
parents: 40774
diff changeset
    10
  Option_Cpo
37110
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff changeset
    11
  Stream
37111
3f84f1f4de64 move HOLCF/Sum_Cpo.thy to HOLCF/Library
huffman
parents: 37110
diff changeset
    12
  Sum_Cpo
37110
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff changeset
    13
begin
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff changeset
    14
7ffdbc24b27f move Strict_Fun and Stream theories to new HOLCF/Library directory; add HOLCF/Library to search path
huffman
parents:
diff changeset
    15
end