src/Pure/Pure.thy
changeset 70143 0cc7fe616924
parent 70056 25c0ad612d62
child 70177 b67bab2b132c
--- 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"