equal
deleted
inserted
replaced
1 (* Title: CTT/ROOT |
1 (* Title: CTT/ROOT |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1991 University of Cambridge |
4 Copyright 1991 University of Cambridge |
5 |
5 |
6 Adds Constructive Type Theory to a database containing pure Isabelle. |
6 Adds Constructive Type Theory to a database containing pure Isabelle. |
7 Should be executed in the subdirectory CTT. |
7 Should be executed in the subdirectory CTT. |
8 *) |
8 *) |
21 use_thy "Bool"; |
21 use_thy "Bool"; |
22 |
22 |
23 use "../Pure/install_pp.ML"; |
23 use "../Pure/install_pp.ML"; |
24 print_depth 8; |
24 print_depth 8; |
25 |
25 |
26 val CTT_build_completed = (); (*indicate successful build*) |
26 val CTT_build_completed = (); (*indicate successful build*) |