# 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>\x\<^sub>1\ 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 \\<^sub>a* *} +text {* congruence rules for \\\<^sub>a*\ *} lemma ax_do_not_a_star_reduce: shows "Ax x a \\<^sub>a* M \ M = Ax x a"