src/HOL/HOLCF/HOLCF.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 65378 4bb51e6334ed
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
wenzelm@42151
     1
(*  Title:      HOL/HOLCF/HOLCF.thy
clasohm@1479
     2
    Author:     Franz Regensburger
wenzelm@65378
     3
    Author:     Brian Huffman
nipkow@243
     4
wenzelm@16841
     5
HOLCF -- a semantic extension of HOL by the LCF logic.
nipkow@243
     6
*)
nipkow@243
     7
huffman@15650
     8
theory HOLCF
huffman@29130
     9
imports
huffman@35473
    10
  Main
huffman@35473
    11
  Domain
huffman@35473
    12
  Powerdomains
huffman@15650
    13
begin
huffman@15650
    14
huffman@40497
    15
default_sort "domain"
huffman@25904
    16
huffman@15650
    17
end