equal
deleted
inserted
replaced
37 } |
37 } |
38 |
38 |
39 val eval_init = |
39 val eval_init = |
40 if (heaps.isEmpty) { |
40 if (heaps.isEmpty) { |
41 List( |
41 List( |
|
42 "val ML_file = PolyML.use", |
42 if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") "structure FixedInt = IntInf" |
43 if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") "structure FixedInt = IntInf" |
43 else "", |
44 else "", |
44 if (Platform.is_windows) |
45 if (Platform.is_windows) |
45 "fun exit 0 = OS.Process.exit OS.Process.success" + |
46 "fun exit 0 = OS.Process.exit OS.Process.success" + |
46 " | exit 1 = OS.Process.exit OS.Process.failure" + |
47 " | exit 1 = OS.Process.exit OS.Process.failure" + |