isabelle: src/CTT/ROOT.ML@57f19fad8c2a (annotated)

1459 d12da312eff4 expanded tabs clasohm parents: 1361 diff changeset	1	(* Title: CTT/ROOT
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	2	ID: $Id$
1459 d12da312eff4 expanded tabs clasohm parents: 1361 diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	4	Copyright 1991 University of Cambridge
a5a9c433f639 Initial revision clasohm parents: diff changeset	5
a5a9c433f639 Initial revision clasohm parents: diff changeset	6	Adds Constructive Type Theory to a database containing pure Isabelle.
a5a9c433f639 Initial revision clasohm parents: diff changeset	7	Should be executed in the subdirectory CTT.
a5a9c433f639 Initial revision clasohm parents: diff changeset	8	*)
a5a9c433f639 Initial revision clasohm parents: diff changeset	9
a5a9c433f639 Initial revision clasohm parents: diff changeset	10	val banner = "Constructive Type Theory";
a5a9c433f639 Initial revision clasohm parents: diff changeset	11	writeln banner;
a5a9c433f639 Initial revision clasohm parents: diff changeset	12
10466 78168ca70469 new Main.thy as in HOL, ZF paulson parents: 6349 diff changeset	13	use_thy "Main";
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	14
10466 78168ca70469 new Main.thy as in HOL, ZF paulson parents: 6349 diff changeset	15	Goal "tt : T"; (leave subgoal package empty)