src/HOL/HOLCF/ex/Domain_Proofs.thy
changeset 58880 0baae4311a9f
parent 49759 ecf1d5d87e5e
child 61424 c3658c18b7bc
equal deleted inserted replaced
58879:143c85e3cdb5 58880:0baae4311a9f
     1 (*  Title:      HOL/HOLCF/ex/Domain_Proofs.thy
     1 (*  Title:      HOL/HOLCF/ex/Domain_Proofs.thy
     2     Author:     Brian Huffman
     2     Author:     Brian Huffman
     3 *)
     3 *)
     4 
     4 
     5 header {* Internal domain package proofs done manually *}
     5 section {* Internal domain package proofs done manually *}
     6 
     6 
     7 theory Domain_Proofs
     7 theory Domain_Proofs
     8 imports HOLCF
     8 imports HOLCF
     9 begin
     9 begin
    10 
    10