author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 42151  4da4fc77664b 
child 58880  0baae4311a9f 
permissions  rwrr 
42151  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 