src/HOL/MicroJava/ROOT.ML
changeset 10611 e460c53c1c9b
parent 10047 8f228c148456
child 10631 591ea23d27a0
equal deleted inserted replaced
10610:1dc640d06d19 10611:e460c53c1c9b
     2 goals_limit := 1;
     2 goals_limit := 1;
     3 
     3 
     4 Unify.search_bound := 40;
     4 Unify.search_bound := 40;
     5 Unify.trace_bound  := 40;
     5 Unify.trace_bound  := 40;
     6 
     6 
     7 with_paths ["J", "JVM", "BV"] use_thy "Digest"; 
     7 add_path "J";
       
     8 add_path "JVM";
       
     9 add_path "BV";
       
    10 use_thy "Digest";