author | wenzelm |
Mon, 26 Jun 2000 00:00:40 +0200 | |
changeset 9143 | 6180c29d2db6 |
parent 9142 | d5a841f89e92 |
child 9144 | 20a70ef9c320 |
--- a/src/HOL/MicroJava/ROOT.ML Sun Jun 25 23:58:54 2000 +0200 +++ b/src/HOL/MicroJava/ROOT.ML Mon Jun 26 00:00:40 2000 +0200 @@ -1,8 +1,8 @@ -goals_limit:=1; +goals_limit := 1; Unify.search_bound := 40; Unify.trace_bound := 40; -with_path "J" (with_path "JVM" (with_path "BV" use_thy)) "JTypeSafe"; -with_path "J" (with_path "JVM" (with_path "BV" use_thy)) "BVSpecTypeSafe"; +with_paths ["J", "JVM", "BV"] use_thy "JTypeSafe"; +with_paths ["J", "JVM", "BV"] use_thy "BVSpecTypeSafe";