refined antiquotation interface: formally pass result context and (potential) result source;
removed redundant raw_antiquotation;
\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: