\input{Base.tex} \input{Integration.tex} \input{Isar.tex} \input{Local_Theory.tex} \input{Logic.tex} \input{ML.tex} \input{Prelim.tex} \input{Proof.tex} \input{Syntax.tex} \input{Tactic.tex} %%% Local Variables: %%% mode: latex %%% TeX-master: "root" %%% End: