doc-src/TutorialI/Recdef/document/Induction.tex
changeset 17181 5f42dd5e6570
parent 17175 1eced27ee0e1
child 17187 45bee2f6e61f
equal deleted inserted replaced
17180:5fefe658a6f8 17181:5f42dd5e6570
     1 %
     1 %
     2 \begin{isabellebody}%
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Induction}%
     3 \def\isabellecontext{Induction}%
       
     4 \isamarkupfalse%
     4 %
     5 %
     5 \isadelimtheory
     6 \isadelimtheory
     6 %
     7 %
     7 \endisadelimtheory
     8 \endisadelimtheory
     8 %
     9 %
     9 \isatagtheory
    10 \isatagtheory
    10 \isamarkupfalse%
       
    11 %
    11 %
    12 \endisatagtheory
    12 \endisatagtheory
    13 {\isafoldtheory}%
    13 {\isafoldtheory}%
    14 %
    14 %
    15 \isadelimtheory
    15 \isadelimtheory
   106 \isadelimtheory
   106 \isadelimtheory
   107 %
   107 %
   108 \endisadelimtheory
   108 \endisadelimtheory
   109 %
   109 %
   110 \isatagtheory
   110 \isatagtheory
   111 \isamarkupfalse%
       
   112 %
   111 %
   113 \endisatagtheory
   112 \endisatagtheory
   114 {\isafoldtheory}%
   113 {\isafoldtheory}%
   115 %
   114 %
   116 \isadelimtheory
   115 \isadelimtheory