diff -r a6ca869af096 -r b219774a71ae src/Pure/General/path.scala --- a/src/Pure/General/path.scala Wed Mar 31 21:44:29 2021 +0200 +++ b/src/Pure/General/path.scala Wed Mar 31 22:10:56 2021 +0200 @@ -87,6 +87,9 @@ def variable(s: String): Path = new Path(List(variable_elem(s))) val parent: Path = new Path(List(Parent)) + val USER_HOME: Path = variable("USER_HOME") + val ISABELLE_HOME: Path = variable("ISABELLE_HOME") + /* explode */