1
goals_limit := 1;
2
3
add_path "J";
4
add_path "JVM";
5
add_path "BV";
6
7
use_thy "JTypeSafe";
8
use_thy "Example";
9
use_thy "BVSpecTypeSafe";
10
use_thy "LBVCorrect";
11
use_thy "LBVComplete";
12
use_thy "JVM";