\input{base.tex} \input{prelim.tex} \input{logic.tex} \input{tactic.tex} \input{proof.tex} \input{isar.tex} \input{locale.tex} \input{integration.tex} \input{ML.tex} %%% Local Variables: %%% mode: latex %%% TeX-master: "root" %%% End: