src/HOL/MicroJava/ROOT.ML

invoke_case: include attributes;

goals_limit:=1;

Unify.search_bound := 40;
Unify.trace_bound  := 40;

add_path "J";
add_path "JVM";
add_path "BV";


use_thy "JTypeSafe";
use_thy "BVSpecTypeSafe";