# HG changeset patch
# User wenzelm
# Date 1604087128 -3600
# Node ID f760554a5a295ef3847de38be64a03d2c6e3abf4
# Parent  4be6ae020fc4faf7b36eb597ec3cc9fdd7165c1d
tuned;

diff -r 4be6ae020fc4 -r f760554a5a29 src/Doc/System/Phabricator.thy
--- a/src/Doc/System/Phabricator.thy	Thu Oct 29 16:07:41 2020 +0100
+++ b/src/Doc/System/Phabricator.thy	Fri Oct 30 20:45:28 2020 +0100
@@ -73,8 +73,8 @@
   (\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
@@ -212,7 +212,7 @@
 \<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