- declared wf_java_prog as syntax (previously: definition)
- in wf_java_mdecl: added preconditions for 'This'
- rule LAss: precondition v ~=This
goals_limit := 1;
add_path "J";
add_path "JVM";
add_path "BV";
use_thy "JTypeSafe";
use_thy "Example";
use_thy "BVSpecTypeSafe";
use_thy "LBVCorrect";
use_thy "LBVComplete";
use_thy "JVM";