--- a/src/Pure/Pure.thy Sat Apr 13 12:45:38 2019 +0200
+++ b/src/Pure/Pure.thy Sat Apr 13 13:30:02 2019 +0200
@@ -95,7 +95,8 @@
and "extract_type" "extract" :: thy_decl
and "find_theorems" "find_consts" :: diag
and "named_theorems" :: thy_decl
-abbrevs "===>" = "===>" (*prevent replacement of very long arrows*)
+abbrevs "\\tag" = "\<^marker>\<open>tag \<close>"
+ and "===>" = "===>" (*prevent replacement of very long arrows*)
and "--->" = "\<midarrow>\<rightarrow>"
and "hence" "thus" "default_sort" "simproc_setup" "apply_end" "realizers" "realizability" = ""
and "hence" = "then have"