doc-src/TutorialI/Advanced/document/simp.tex
changeset 17056 05fc32a23b8b
parent 14270 342451d763f9
child 17175 1eced27ee0e1
equal deleted inserted replaced
17055:eacce1cd716a 17056:05fc32a23b8b
     1 %
     1 %
     2 \begin{isabellebody}%
     2 \begin{isabellebody}%
     3 \def\isabellecontext{simp}%
     3 \def\isabellecontext{simp}%
     4 \isamarkupfalse%
     4 %
       
     5 \isadelimtheory
       
     6 %
       
     7 \endisadelimtheory
       
     8 %
       
     9 \isatagtheory
       
    10 %
       
    11 \endisatagtheory
       
    12 {\isafoldtheory}%
       
    13 %
       
    14 \isadelimtheory
       
    15 %
       
    16 \endisadelimtheory
       
    17 \isamarkuptrue%
     5 %
    18 %
     6 \isamarkupsection{Simplification%
    19 \isamarkupsection{Simplification%
     7 }
    20 }
     8 \isamarkuptrue%
    21 \isamarkuptrue%
     9 %
    22 %
   214 \isa{p\ {\isasymLongrightarrow}\ t\ {\isacharequal}\ u},\quad  \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ False},\quad  \isa{s\ {\isacharequal}\ True}.
   227 \isa{p\ {\isasymLongrightarrow}\ t\ {\isacharequal}\ u},\quad  \isa{p\ {\isasymLongrightarrow}\ r\ {\isacharequal}\ False},\quad  \isa{s\ {\isacharequal}\ True}.
   215 \end{center}
   228 \end{center}
   216 \index{simplification rule|)}
   229 \index{simplification rule|)}
   217 \index{simplification|)}%
   230 \index{simplification|)}%
   218 \end{isamarkuptext}%
   231 \end{isamarkuptext}%
   219 \isamarkuptrue%
   232 %
   220 \isamarkupfalse%
   233 \isadelimtheory
       
   234 %
       
   235 \endisadelimtheory
       
   236 %
       
   237 \isatagtheory
       
   238 %
       
   239 \endisatagtheory
       
   240 {\isafoldtheory}%
       
   241 %
       
   242 \isadelimtheory
       
   243 %
       
   244 \endisadelimtheory
   221 \end{isabellebody}%
   245 \end{isabellebody}%
   222 %%% Local Variables:
   246 %%% Local Variables:
   223 %%% mode: latex
   247 %%% mode: latex
   224 %%% TeX-master: "root"
   248 %%% TeX-master: "root"
   225 %%% End:
   249 %%% End: