src/HOL/HOLCF/HOLCF.thy
author haftmann
Sun Jun 23 21:16:07 2013 +0200 (2013-06-23)
changeset 52435 6646bb548c6b
parent 45049 13efaee97111
child 65378 4bb51e6334ed
permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/HOLCF.thy
clasohm@1479
     2
    Author:     Franz Regensburger
nipkow@243
     3
wenzelm@16841
     4
HOLCF -- a semantic extension of HOL by the LCF logic.
nipkow@243
     5
*)
nipkow@243
     6
huffman@15650
     7
theory HOLCF
huffman@29130
     8
imports
huffman@35473
     9
  Main
huffman@35473
    10
  Domain
huffman@35473
    11
  Powerdomains
huffman@15650
    12
begin
huffman@15650
    13
huffman@40497
    14
default_sort "domain"
huffman@25904
    15
huffman@15650
    16
end