src/Cube/ex/ROOT.ML
changeset 17260 df7c3b1f390a
parent 9000 c20d58286a51
equal deleted inserted replaced
17259:dda237f1d299 17260:df7c3b1f390a
       
     1 
       
     2 (* $Id$ *)
     1 
     3 
     2 time_use_thy "ex";
     4 time_use_thy "ex";