src/HOL/HOLCF/Plain_HOLCF.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: 40774
diff changeset
     1
(*  Title:      HOL/HOLCF/Plain_HOLCF.thy
40502
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
     2
    Author:     Brian Huffman
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
     3
*)
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
     4
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
     5
header {* Plain HOLCF *}
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
     6
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
     7
theory Plain_HOLCF
40592
f432973ce0f6 move strict function type into main HOLCF; instance cfun :: (predomain, domain) domain
huffman
parents: 40502
diff changeset
     8
imports Cfun Sfun Cprod Sprod Ssum Up Discrete Lift One Tr Fix
40502
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
     9
begin
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
    10
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
    11
text {*
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
    12
  Basic HOLCF concepts and types; does not include definition packages.
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
    13
*}
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
    14
8e92772bc0e8 move map functions to new theory file Map_Functions; add theory file Plain_HOLCF
huffman
parents:
diff changeset
    15
end