--- a/NEWS Sat Apr 13 12:45:38 2019 +0200
+++ b/NEWS Sat Apr 13 13:30:02 2019 +0200
@@ -131,6 +131,9 @@
statement by default (e.g. 'theorem', 'lemma'). This is a subtle change
of semantics wrt. old-style %name.
+* In Isabelle/jEdit, the string "\tag" may be completed to a "\<^marker>\<open>tag \<close>"
+template.
+
* Document antiquotation option "cartouche" indicates if the output
should be delimited as cartouche; this takes precedence over the
analogous option "quotes".
--- 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"