retain important whitespace after 'text' that is suppressed, but swallows adjacent whitespace;
authorwenzelm
Tue Jan 01 20:57:54 2019 +0100 (6 months ago)
changeset 695651daf07b65385
parent 69564 a59f7d07bf17
child 69566 c41954ee87cf
retain important whitespace after 'text' that is suppressed, but swallows adjacent whitespace;
src/HOL/Analysis/Continuum_Not_Denumerable.thy
src/HOL/Analysis/Infinite_Products.thy
src/HOL/Analysis/Norm_Arith.thy
src/HOL/Analysis/Path_Connected.thy
src/HOL/Analysis/Tagged_Division.thy
     1.1 --- a/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Tue Jan 01 13:26:37 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Continuum_Not_Denumerable.thy	Tue Jan 01 20:57:54 2019 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4    range of \<open>f\<close> by generating a sequence of closed intervals then using the
     1.5    Nested Interval Property.
     1.6  \<close>
     1.7 -
     1.8 +text%important \<open>%whitespace\<close>
     1.9  theorem real_non_denum: "\<nexists>f :: nat \<Rightarrow> real. surj f"
    1.10  proof
    1.11    assume "\<exists>f::nat \<Rightarrow> real. surj f"
     2.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Tue Jan 01 13:26:37 2019 +0100
     2.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Tue Jan 01 20:57:54 2019 +0100
     2.3 @@ -58,6 +58,7 @@
     2.4    where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
     2.5  
     2.6  text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
     2.7 +text%important \<open>%whitespace\<close>
     2.8  definition%important
     2.9    has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
    2.10    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)"
     3.1 --- a/src/HOL/Analysis/Norm_Arith.thy	Tue Jan 01 13:26:37 2019 +0100
     3.2 +++ b/src/HOL/Analysis/Norm_Arith.thy	Tue Jan 01 20:57:54 2019 +0100
     3.3 @@ -137,7 +137,7 @@
     3.4  
     3.5  
     3.6  text \<open>Hence more metric properties.\<close>
     3.7 -
     3.8 +text%important \<open>%whitespace\<close>
     3.9  proposition dist_triangle_add:
    3.10    fixes x y x' y' :: "'a::real_normed_vector"
    3.11    shows "dist (x + y) (x' + y') \<le> dist x x' + dist y y'"
     4.1 --- a/src/HOL/Analysis/Path_Connected.thy	Tue Jan 01 13:26:37 2019 +0100
     4.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Tue Jan 01 20:57:54 2019 +0100
     4.3 @@ -3401,12 +3401,12 @@
     4.4         (\<forall>x. h(1, x) = q x) \<and>
     4.5         (\<forall>t \<in> {0..1}. P(\<lambda>x. h(t, x))))"
     4.6  
     4.7 -
     4.8  text\<open>$p, q$ are functions $X \to Y$, and the property $P$ restricts all intermediate maps.
     4.9  We often just want to require that $P$ fixes some subset, but to include the case of a loop homotopy,
    4.10  it is convenient to have a general property $P$.\<close>
    4.11  
    4.12  text \<open>We often want to just localize the ending function equality or whatever.\<close>
    4.13 +text%important \<open>%whitespace\<close>
    4.14  proposition homotopic_with:
    4.15    fixes X :: "'a::topological_space set" and Y :: "'b::topological_space set"
    4.16    assumes "\<And>h k. (\<And>x. x \<in> X \<Longrightarrow> h x = k x) \<Longrightarrow> (P h \<longleftrightarrow> P k)"
     5.1 --- a/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 01 13:26:37 2019 +0100
     5.2 +++ b/src/HOL/Analysis/Tagged_Division.thy	Tue Jan 01 20:57:54 2019 +0100
     5.3 @@ -1293,7 +1293,7 @@
     5.4    @{typ bool}.\<close>
     5.5  
     5.6  paragraph%important \<open>Using additivity of lifted function to encode definedness.\<close>
     5.7 -
     5.8 +text%important \<open>%whitespace\<close>
     5.9  definition%important lift_option :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a option \<Rightarrow> 'b option \<Rightarrow> 'c option"
    5.10  where
    5.11    "lift_option f a' b' = Option.bind a' (\<lambda>a. Option.bind b' (\<lambda>b. Some (f a b)))"
    5.12 @@ -1334,7 +1334,7 @@
    5.13  
    5.14  
    5.15  paragraph \<open>Division points\<close>
    5.16 -
    5.17 +text%important \<open>%whitespace\<close>
    5.18  definition%important "division_points (k::('a::euclidean_space) set) d =
    5.19     {(j,x). j \<in> Basis \<and> (interval_lowerbound k)\<bullet>j < x \<and> x < (interval_upperbound k)\<bullet>j \<and>
    5.20       (\<exists>i\<in>d. (interval_lowerbound i)\<bullet>j = x \<or> (interval_upperbound i)\<bullet>j = x)}"