LaTeX code is now generated directly from Even and Advanced theories.
authorberghofe
Thu, 19 Jul 2007 15:30:35 +0200
changeset 238434cd60e5d2999
parent 23842 9d87177f1f89
child 23844 7da8f260d920
LaTeX code is now generated directly from Even and Advanced theories.
doc-src/TutorialI/Inductive/inductive.tex
     1.1 --- a/doc-src/TutorialI/Inductive/inductive.tex	Thu Jul 19 15:29:51 2007 +0200
     1.2 +++ b/doc-src/TutorialI/Inductive/inductive.tex	Thu Jul 19 15:30:35 2007 +0200
     1.3 @@ -13,13 +13,13 @@
     1.4  context-free grammars. The first two sections are required reading for anybody
     1.5  interested in mathematical modelling.
     1.6  
     1.7 -\input{Inductive/even-example}
     1.8 +\input{Inductive/document/Even}
     1.9  \input{Inductive/document/Mutual}
    1.10  \input{Inductive/document/Star}
    1.11  
    1.12  \section{Advanced Inductive Definitions}
    1.13  \label{sec:adv-ind-def}
    1.14 -\input{Inductive/advanced-examples}
    1.15 +\input{Inductive/document/Advanced}
    1.16  
    1.17  \input{Inductive/document/AB}
    1.18