more direct use of latex tools: avoid diversion into "isabelle latex -o pdf" and its confusion of ISABELLE_PDFLATEX vs. ISABELLE_LUALATEX;
clarified ISABELLE_MAKEINDEX options;
chapter Tools
session Tools = Pure +
theories
Code_Generator
session Spec_Check in Spec_Check = Pure +
theories
Spec_Check
Examples
session SML in SML = Pure +
theories
Examples
session Haskell in Haskell = Pure +
theories
Haskell
theories [condition = ISABELLE_GHC_STACK]
Test