retain important whitespace after 'text' that is suppressed, but swallows adjacent whitespace;

--- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Tue Jan 01 13:26:37 2019 +0100
+++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Tue Jan 01 20:57:54 2019 +0100
@@ -32,7 +32,7 @@
   range of \<open>f\<close> by generating a sequence of closed intervals then using the
   Nested Interval Property.
 \<close>
-
+text%important \<open>%whitespace\<close>
 theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
 proof
   assume "\<exists>f::nat \<Rightarrow> real. surj f"

--- a/src/HOL/Analysis/Infinite_Products.thy	Tue Jan 01 13:26:37 2019 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy	Tue Jan 01 20:57:54 2019 +0100
@@ -58,6 +58,7 @@
   where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
 
 text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
+text%important \<open>%whitespace\<close>
 definition%important
   has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
   where "f has_prod p \<equiv> raw_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> raw_has_prod f (Suc i) q)"

--- a/src/HOL/Analysis/Norm_Arith.thy	Tue Jan 01 13:26:37 2019 +0100
+++ b/src/HOL/Analysis/Norm_Arith.thy	Tue Jan 01 20:57:54 2019 +0100
@@ -137,7 +137,7 @@
 
 
 text \<open>Hence more metric properties.\<close>
-
+text%important \<open>%whitespace\<close>
 proposition dist_triangle_add:
   fixes x y x' y' :: "'a::real_normed_vector"
   shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"

--- a/src/HOL/Analysis/Path_Connected.thy	Tue Jan 01 13:26:37 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jan 01 20:57:54 2019 +0100
@@ -3401,12 +3401,12 @@
        (\<forall>x. h(1, x) = q x) \<and>
        (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
 
-
 text\<open>$p, q$ are functions $X \to Y$, and the property $P$ restricts all intermediate maps.
 We often just want to require that $P$ fixes some subset, but to include the case of a loop homotopy,
 it is convenient to have a general property $P$.\<close>
 
 text \<open>We often want to just localize the ending function equality or whatever.\<close>
+text%important \<open>%whitespace\<close>
 proposition homotopic_with:
   fixes X :: "'a::topological_space set" and Y :: "'b::topological_space set"
   assumes "\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"

--- a/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 01 13:26:37 2019 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 01 20:57:54 2019 +0100
@@ -1293,7 +1293,7 @@
   @{typ bool}.\<close>
 
 paragraph%important \<open>Using additivity of lifted function to encode definedness.\<close>
-
+text%important \<open>%whitespace\<close>
 definition%important lift_option :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 'c option"
 where
   "lift_option f a' b' = Option.bind a' (\<lambda>a. Option.bind b' (\<lambda>b. Some (f a b)))"
@@ -1334,7 +1334,7 @@
 
 
 paragraph \<open>Division points\<close>
-
+text%important \<open>%whitespace\<close>
 definition%important "division_points (k::('a::euclidean_space) set) d =
    {(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
      (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"