doc-src/LaTeXsugar/Sugar/document/Sugar.tex
changeset 16396 d9d2a0cadd5e
parent 16176 ef83d8e097ba
child 17125 e6a82d1a1829
equal deleted inserted replaced
16395:3446d2b6a19f 16396:d9d2a0cadd5e
   150 internal index. This can be avoided by turning the last digit into a
   150 internal index. This can be avoided by turning the last digit into a
   151 subscript: write \verb!x\<^isub>1! and obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.%
   151 subscript: write \verb!x\<^isub>1! and obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.%
   152 \end{isamarkuptext}%
   152 \end{isamarkuptext}%
   153 \isamarkuptrue%
   153 \isamarkuptrue%
   154 \isamarkupfalse%
   154 \isamarkupfalse%
       
   155 %
       
   156 \isamarkupsubsection{Variable names%
       
   157 }
       
   158 \isamarkuptrue%
       
   159 %
       
   160 \begin{isamarkuptext}%
       
   161 It sometimes happens that you want to change the name of a
       
   162 variable in a theorem before printing it. This can easily be achieved
       
   163 with the help of Isabelle's instantiation attribute \texttt{where}:
       
   164 \isa{{\isasymlbrakk}{\isasymphi}{\isacharsemicolon}\ {\isasympsi}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isasymand}\ {\isasympsi}} is the result of
       
   165 \begin{quote}
       
   166 \verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
       
   167 \end{quote}
       
   168 To support the ``\_''-notation for irrelevant variables
       
   169 the constant \texttt{DUMMY} has been introduced:
       
   170 \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ \_{\isacharparenright}\ {\isacharequal}\ a} is produced by
       
   171 \begin{quote}
       
   172 \verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
       
   173 \end{quote}%
       
   174 \end{isamarkuptext}%
       
   175 \isamarkuptrue%
   155 %
   176 %
   156 \isamarkupsubsection{Inference rules%
   177 \isamarkupsubsection{Inference rules%
   157 }
   178 }
   158 \isamarkuptrue%
   179 \isamarkuptrue%
   159 %
   180 %