# HG changeset patch
# User nipkow
# Date 1739009910 -3600
# Node ID eebb8270b3cc1ca36d71b54dac7813e711d9d98c
# Parent  15261d78d7b5c8a6b6cb776002ae513fb5440ce8
more syntax update

diff -r 15261d78d7b5 -r eebb8270b3cc src/Doc/Sugar/Sugar.thy
--- a/src/Doc/Sugar/Sugar.thy	Fri Feb 07 21:27:11 2025 +0100
+++ b/src/Doc/Sugar/Sugar.thy	Sat Feb 08 11:18:30 2025 +0100
@@ -533,9 +533,9 @@
 You have to place the following lines before and after the snippet, where snippets must always be
 consecutive lines of theory text:
 \begin{quote}
-\verb!\text_raw{!\verb!*\snip{!\emph{snippetname}\verb!}{1}{2}{%*!\verb!}!\\
+\verb!\text_raw\!\verb!<open>\snip{!\emph{snippetname}\verb!}{1}{2}{%\!\verb!<close>!\\
 \emph{theory text}\\
-\verb!\text_raw{!\verb!*!\verb!}%endsnip*!\verb!}!
+\verb!\text_raw\!\verb!<open>%endsnip\!\verb!<close>!
 \end{quote}
 where \emph{snippetname} should be a unique name for the snippet. The numbers \texttt{1}
 and \texttt{2} are explained in a moment.