doc-src/IsarRef/Thy/document/ML_Tactic.tex
changeset 30240 5b25fee0362c
parent 27249 f339dc43ce9f
child 40406 313a24b66a8d
equal deleted inserted replaced
30239:179ff9cb160b 30240:5b25fee0362c
     1 %
     1 %
     2 \begin{isabellebody}%
     2 \begin{isabellebody}%
     3 \def\isabellecontext{ML{\isacharunderscore}Tactic}%
     3 \def\isabellecontext{ML{\isacharunderscore}Tactic}%
     4 %
     4 %
     5 \isadelimtheory
     5 \isadelimtheory
     6 \isanewline
       
     7 \isanewline
       
     8 %
     6 %
     9 \endisadelimtheory
     7 \endisadelimtheory
    10 %
     8 %
    11 \isatagtheory
     9 \isatagtheory
    12 \isacommand{theory}\isamarkupfalse%
    10 \isacommand{theory}\isamarkupfalse%