equal
deleted
inserted
replaced
1 (* Title: LCF/ROOT |
1 (* Title: LCF/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 Adds LCF to a database containing First-Order Logic. |
6 LCF on top of First-Order Logic. |
7 |
7 |
8 This theory is based on Lawrence Paulson's book Logic and Computation. |
8 This theory is based on Lawrence Paulson's book Logic and Computation. |
9 *) |
9 *) |
10 |
10 |
11 val banner = "Logic for Computable Functions (in FOL)"; |
11 val banner = "Logic for Computable Functions (in FOL)"; |