equal
deleted
inserted
replaced
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 classes cpo < "term" |
17 defaultsort cpo |
17 default_sort cpo |
18 |
18 |
19 typedecl tr |
19 typedecl tr |
20 typedecl void |
20 typedecl void |
21 typedecl ('a,'b) "*" (infixl "*" 6) |
21 typedecl ('a,'b) "*" (infixl "*" 6) |
22 typedecl ('a,'b) "+" (infixl "+" 5) |
22 typedecl ('a,'b) "+" (infixl "+" 5) |