954   \end{tabular}}

   954   \end{tabular}}

   955   \end{isabelle}

   955   \end{isabelle}

   956   

   956   

   957   \noindent

   957   \noindent

   958   generating an optional value.

   958   generating an optional value.

   960   root}-directory is always its own anchor unless it has been

   960   root}-directory is always its own anchor unless it has been

   961   deleted. If a file is present in the initial state and not deleted

   961   deleted. If a file is present in the initial state and not deleted

   962   in @{text s}, then it is also its own anchor, otherwise the anchor

   962   in @{text s}, then it is also its own anchor, otherwise the anchor

   963   will be the anchor of the parent directory.  For example if we have

   963   will be the anchor of the parent directory.  For example if we have

   964   a directory @{text pf} in the initial state, then its anchor is @{text "Some pf"}

   964   a directory @{text pf} in the initial state, then its anchor is @{text "Some pf"}