equal
deleted
inserted
replaced
21 |
21 |
22 val chapter: String = "AFP" |
22 val chapter: String = "AFP" |
23 |
23 |
24 val force_partition1: List[String] = List("Category3", "HOL-ODE") |
24 val force_partition1: List[String] = List("Category3", "HOL-ODE") |
25 |
25 |
26 def init(options: Options, base_dir: Path = Path.explode("$AFP_BASE")): AFP = |
26 val BASE: Path = Path.explode("$AFP_BASE") |
|
27 |
|
28 def init(options: Options, base_dir: Path = BASE): AFP = |
27 new AFP(options, base_dir) |
29 new AFP(options, base_dir) |
28 |
30 |
29 |
31 |
30 /* entries */ |
32 /* entries */ |
31 |
33 |