src/HOL/MiniML/ROOT.ML
changeset 1925 1150f128c7fe
parent 1351 4a960c012383
child 2031 03a843f0f447
equal deleted inserted replaced
1924:0f1a583457da 1925:1150f128c7fe
     9 HOL_build_completed;	(*Make examples fail if HOL did*)
     9 HOL_build_completed;	(*Make examples fail if HOL did*)
    10 
    10 
    11 writeln"Root file for HOL/MiniML";
    11 writeln"Root file for HOL/MiniML";
    12 Unify.trace_bound := 20;
    12 Unify.trace_bound := 20;
    13 
    13 
       
    14 AddSEs [less_SucE];
       
    15 
    14 time_use_thy "I";
    16 time_use_thy "I";