(* Title: CTT/ROOT.ML ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1991 University of Cambridge *) val banner = "Constructive Type Theory"; writeln banner; use_thy "Main";