equal
deleted
inserted
replaced
6 |
6 |
7 header {* LCF on top of First-Order Logic *} |
7 header {* LCF on top of First-Order Logic *} |
8 |
8 |
9 theory LCF |
9 theory LCF |
10 imports FOL |
10 imports FOL |
11 uses ("pair.ML") ("fix.ML") |
11 uses ("LCF_lemmas.ML") ("pair.ML") ("fix.ML") |
12 begin |
12 begin |
13 |
13 |
14 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *} |
14 text {* This theory is based on Lawrence Paulson's book Logic and Computation. *} |
15 |
15 |
16 subsection {* Natural Deduction Rules for LCF *} |
16 subsection {* Natural Deduction Rules for LCF *} |