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/Norm_Arith.thy
changeset 70136 f03a01a18c6e
parent 69605 a96320074298 
--- a/src/HOL/Analysis/Norm_Arith.thy	Fri Apr 12 19:48:29 2019 +0200
+++ b/src/HOL/Analysis/Norm_Arith.thy	Fri Apr 12 22:09:25 2019 +0200
@@ -131,13 +131,13 @@
 
 ML_file \<open>normarith.ML\<close>
 
-method_setup%important norm = \<open>
+method_setup\<^marker>\<open>tag important\<close> norm = \<open>
   Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
 \<close> "prove simple linear statements about vector norms"
 
 
 text \<open>Hence more metric properties.\<close>
-text%important \<open>%whitespace\<close>
+text\<^marker>\<open>tag important\<close> \<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'"
isabelle