# HG changeset patch
# User wenzelm
# Date 1446849071 -3600
# Node ID 07a903c8cc916a9f165d636910806bf0846802ae
# Parent  810486f886bf06432c8906ca0df731d4f91f8a5b
more antiquotations;

diff -r 810486f886bf -r 07a903c8cc91 src/Doc/Sugar/Sugar.thy
--- a/src/Doc/Sugar/Sugar.thy	Fri Nov 06 21:49:02 2015 +0100
+++ b/src/Doc/Sugar/Sugar.thy	Fri Nov 06 23:31:11 2015 +0100
@@ -137,7 +137,7 @@
 suppresses question marks; variables that end in digits,
 e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
 e.g. @{text"x1.0"}, their internal index. This can be avoided by
-turning the last digit into a subscript: write \verb!x\<^sub>1! and
+turning the last digit into a subscript: write \<^verbatim>\<open>x\<^sub>1\<close> and
 obtain the much nicer @{text"x\<^sub>1"}. *}
 
 (*<*)declare [[show_question_marks = false]](*>*)
diff -r 810486f886bf -r 07a903c8cc91 src/HOL/Nominal/Examples/Class1.thy
--- a/src/HOL/Nominal/Examples/Class1.thy	Fri Nov 06 21:49:02 2015 +0100
+++ b/src/HOL/Nominal/Examples/Class1.thy	Fri Nov 06 23:31:11 2015 +0100
@@ -5189,7 +5189,7 @@
 using a2 a1
 by (induct) (auto)
 
-text {* congruence rules for \<longrightarrow>\<^sub>a* *}
+text {* congruence rules for \<open>\<longrightarrow>\<^sub>a*\<close> *}
 
 lemma ax_do_not_a_star_reduce:
   shows "Ax x a \<longrightarrow>\<^sub>a* M \<Longrightarrow> M = Ax x a"