equal
deleted
inserted
replaced
|
1 (* Title: CTT/ROOT |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Adds Constructive Type Theory to a database containing pure Isabelle. |
|
7 Should be executed in the subdirectory CTT. |
|
8 *) |
|
9 |
|
10 val banner = "Constructive Type Theory"; |
|
11 writeln banner; |
|
12 |
|
13 print_depth 1; |
|
14 |
|
15 use_thy"ctt"; |
|
16 use "../Provers/typedsimp.ML"; |
|
17 use "rew.ML"; |
|
18 use_thy "arith"; |
|
19 use_thy "bool"; |
|
20 |
|
21 use "../Pure/install_pp.ML"; |
|
22 print_depth 8; |
|
23 |
|
24 val CTT_build_completed = (); (*indicate successful build*) |