equal
deleted
inserted
replaced
11 |
11 |
12 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *} |
12 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *} |
13 |
13 |
14 subsection {* Natural Deduction Rules for LCF *} |
14 subsection {* Natural Deduction Rules for LCF *} |
15 |
15 |
16 classes cpo < "term" |
16 class cpo = "term" |
17 default_sort cpo |
17 default_sort cpo |
18 |
18 |
19 typedecl tr |
19 typedecl tr |
20 typedecl void |
20 typedecl void |
21 typedecl ('a,'b) prod (infixl "*" 6) |
21 typedecl ('a,'b) prod (infixl "*" 6) |
22 typedecl ('a,'b) sum (infixl "+" 5) |
22 typedecl ('a,'b) sum (infixl "+" 5) |
23 |
23 |
24 arities |
24 instance "fun" :: (cpo, cpo) cpo .. |
25 "fun" :: (cpo, cpo) cpo |
25 instance prod :: (cpo, cpo) cpo .. |
26 prod :: (cpo, cpo) cpo |
26 instance sum :: (cpo, cpo) cpo .. |
27 sum :: (cpo, cpo) cpo |
27 instance tr :: cpo .. |
28 tr :: cpo |
28 instance void :: cpo .. |
29 void :: cpo |
|
30 |
29 |
31 consts |
30 consts |
32 UU :: "'a" |
31 UU :: "'a" |
33 TT :: "tr" |
32 TT :: "tr" |
34 FF :: "tr" |
33 FF :: "tr" |