equal
deleted
inserted
replaced
1 (* Title: CTT/ROOT |
1 (* Title: CTT/ROOT.ML |
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 |
|
6 Adds Constructive Type Theory to a database containing pure Isabelle. |
|
7 Should be executed in the subdirectory CTT. |
|
8 *) |
5 *) |
9 |
6 |
10 val banner = "Constructive Type Theory"; |
7 val banner = "Constructive Type Theory"; |
11 writeln banner; |
8 writeln banner; |
12 |
9 |
13 use_thy "Main"; |
10 use_thy "Main"; |
14 |
|
15 Goal "tt : T"; (*leave subgoal package empty*) |
|