author | huffman |
Sun, 06 Nov 2005 00:22:03 +0100 | |
changeset 18095 | 4328356ab7e6 |
parent 17441 | 5b5feca0344a |
child 19761 | 5cd82054c2c6 |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: CTT/ROOT |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 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 |
||
10466 | 13 |
use_thy "Main"; |
0 | 14 |
|
10466 | 15 |
Goal "tt : T"; (*leave subgoal package empty*) |