src/Cube/ROOT.ML
changeset 3511 da4dd8b7ced4
parent 2237 f01ac387e82b
child 3941 ea440c63d206
equal deleted inserted replaced
3510:24d235feeb2a 3511:da4dd8b7ced4
     1 (*  Title:      Cube/ROOT
     1 (*  Title:      Cube/ROOT.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     3     Author:     Tobias Nipkow
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 The Lambda-Cube a la Barendregt
     6 The Lambda-Cube a la Barendregt.
     7 *)
     7 *)
     8 
     8 
     9 val banner = "Barendregt's Lambda-Cube";
     9 val banner = "Barendregt's Lambda-Cube";
    10 writeln banner;
    10 writeln banner;
    11 
    11 
    12 init_thy_reader();
    12 print_depth 1;  
    13 
    13 
    14 print_depth 1;  
       
    15 use_thy "Cube";
    14 use_thy "Cube";
    16 
    15 
    17 init_pps ();
       
    18 print_depth 8;
    16 print_depth 8;
    19 
    17 
    20 val Cube_build_completed = ();  (*indicate successful build*)
    18 val Cube_build_completed = ();  (*indicate successful build*)