src/Cube/ROOT.ML
changeset 6349 f7750d816c21
parent 4024 3c056eab237c
child 17252 e352f65d5893
equal deleted inserted replaced
6348:fdcbeaddd5fc 6349:f7750d816c21
    12 print_depth 1;  
    12 print_depth 1;  
    13 
    13 
    14 use_thy "Cube";
    14 use_thy "Cube";
    15 
    15 
    16 print_depth 8;
    16 print_depth 8;
    17 
       
    18 val Cube_build_completed = ();  (*indicate successful build*)