doc-src/IsarOverview/Isar/document/Induction.tex

 \isacommand{by}\ simp\isanewline
 \ \ \isamarkupfalse%
 \isacommand{next}\isanewline
 \ \ \ \ \isamarkupfalse%
 \isacommand{case}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ \ \ %
-\isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isachardoublequote}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isachardoublequote}} \isa{{\isachardoublequote}m\ {\isacharless}\ Suc\ n{\isachardoublequote}}%
+\isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}} \isa{{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}m\ {\isacharless}\ Suc\ n{\isacharbraceleft}{\isacharbackslash}isachardoublequote{\isacharbraceright}}%
 }
 \isanewline
 \ \ \ \ \isamarkupfalse%
 \isacommand{show}\ {\isacharquery}case\ \ \ \ %
 \isamarkupcmt{\isa{P\ m}%