equal
deleted
inserted
replaced
1 (* Title: HOL/ROOT.ML |
1 (* Title: HOL/ROOT.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Adds Classical Higher-order Logic to a database containing Pure Isabelle. |
6 Classical Higher-order Logic. |
7 Should be executed in the subdirectory HOL. |
|
8 *) |
7 *) |
9 |
8 |
10 val banner = "Higher-Order Logic"; |
9 val banner = "Higher-Order Logic"; |
11 writeln banner; |
10 writeln banner; |
12 |
11 |