src/Cube/ROOT.ML
author wenzelm
Tue Jul 31 21:19:23 2007 +0200 (2007-07-31)
changeset 24101 bdcefe679ced
parent 17453 eccff680177d
child 24106 f2965bf954dc
permissions -rw-r--r--
with_charset: setmp_noncritical;
     1 (*  Title:      Cube/ROOT.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1992  University of Cambridge
     5 
     6 The Lambda-Cube a la Barendregt.
     7 *)
     8 
     9 val banner = "Barendregt's Lambda-Cube";
    10 writeln banner;
    11 
    12 use_thy "Cube";
    13 use_thy "Example";