equal
deleted
inserted
replaced
|
1 (* Title: LCF/ROOT |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Adds LCF to a database containing First-Order Logic. |
|
7 |
|
8 This theory is based on Lawrence Paulson's book Logic and Computation. |
|
9 *) |
|
10 |
|
11 val banner = "Logic for Computable Functions (in FOL)"; |
|
12 writeln banner; |
|
13 |
|
14 print_depth 1; |
|
15 use_thy "lcf"; |
|
16 use"simpdata.ML"; |
|
17 use"pair.ML"; |
|
18 use"fix.ML"; |
|
19 |
|
20 val LCF_build_completed = (); (*indicate successful build*) |