doc-src/TutorialI/Makefile
changeset 11400 ddcfdc38090d
parent 9695 ec7d7f877712
child 11428 332347b9b942
equal deleted inserted replaced
11399:1605aeb98fd5 11400:ddcfdc38090d
     8 
     8 
     9 
     9 
    10 ## dependencies
    10 ## dependencies
    11 
    11 
    12 include ../Makefile.in
    12 include ../Makefile.in
       
    13 
       
    14 SEDINDEX = isa-index
    13 
    15 
    14 NAME = tutorial
    16 NAME = tutorial
    15 FILES = tutorial.tex basics.tex fp.tex appendix.tex \
    17 FILES = tutorial.tex basics.tex fp.tex appendix.tex \
    16 	../iman.sty ../ttbox.sty ../extra.sty \
    18 	../iman.sty ../ttbox.sty ../extra.sty \
    17 	isabelle.sty isabellesym.sty ../pdfsetup.sty
    19 	isabelle.sty isabellesym.sty ../pdfsetup.sty