src/Doc/System/Phabricator.thy

   For production use, a proper \<^emph>\<open>Virtual Server\<close> or \<^emph>\<open>Root Server\<close> product
   from a hosting provider will be required, including an Internet Domain Name
   (\secref{sec:phabricator-domain}).
 
   Initial experimentation also works on a local host, e.g.\ via
-  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The public domain \<^verbatim>\<open>lvh.me\<close> is
-  used by default: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
+  VirtualBox\<^footnote>\<open>\<^url>\<open>https://www.virtualbox.org\<close>\<close>. The Internet domain \<^verbatim>\<open>lvh.me\<close>
+  is used by default: it maps arbitrary subdomains to \<^verbatim>\<open>localhost\<close>.
 
   All administrative commands need to be run as \<^verbatim>\<open>root\<close> user (e.g.\ via
   \<^verbatim>\<open>sudo\<close>). Note that Isabelle refers to user-specific configuration in the
   user home directory via @{setting ISABELLE_HOME_USER}
   (\secref{sec:settings}); that may be different or absent for the root user

   The tool can be invoked multiple times with different parameters; ports are
   changed back and forth each time and services restarted.
 \<close>
 
 
-subsection \<open>Public domain name and HTTPS configuration \label{sec:phabricator-domain}\<close>
+subsection \<open>Internet domain name and HTTPS configuration \label{sec:phabricator-domain}\<close>
 
 text \<open>
   So far the Phabricator server has been accessible only on \<^verbatim>\<open>localhost\<close> (via
   the alias \<^verbatim>\<open>lvh.me\<close>). Proper configuration of a public Internet domain name
   (with HTTPS certificate from \<^emph>\<open>Let's Encrypt\<close>) works as follows.