Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Analysis/Integral_Test.thy
changeset 70136 f03a01a18c6e
parent 68643 3db6c9338ec1 
--- a/src/HOL/Analysis/Integral_Test.thy	Fri Apr 12 19:48:29 2019 +0200
+++ b/src/HOL/Analysis/Integral_Test.thy	Fri Apr 12 22:09:25 2019 +0200
@@ -19,7 +19,7 @@
 \<close>
 
 (* TODO: continuous_in \<rightarrow> integrable_on *)
-locale%important antimono_fun_sum_integral_diff =
+locale\<^marker>\<open>tag important\<close> antimono_fun_sum_integral_diff =
   fixes f :: "real \<Rightarrow> real"
   assumes dec: "\<And>x y. x \<ge> 0 \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<ge> f y"
   assumes nonneg: "\<And>x. x \<ge> 0 \<Longrightarrow> f x \<ge> 0"
isabelle