Skip to content

Latest commit

 

History

History

book

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Formal Language Theory: Integrating Experimentation with Proof

This directory contains the LaTeX source for the book. The root file is book.tex.

Run

  latexmk -pdfps book.tex

to generate the PDF version of the book: book.pdf. A copy of latexmk is in this directory.

Modifying the Book

The BASE.eepic files were generated using xfig from the BASE.fig files. Xfig should be started up with the

  -latexfonts -specialtext -exportLanguage eepic

options.

The chap-N.M-forlanL.tex Forlan transcripts were generated from the chap-N.M-forlanL files, using the program smlnjtrans.

This process was automated by the chap-N.M-transcripts shell scripts. To run these scripts, you must have both smlnjtrans and forlan on your search path. The script book-transcripts runs all of the transcripts.

The script cleanup can be used to delete all of the files generated by latex, bibtex, etc.

Run make-and-install-book to generate the book and install in the HTML directory.