1 theory Base

     1 theory Base

     2 imports Main LaTeXsugar

     2 imports Main LaTeXsugar

     3 uses

     3 uses

     4   "output_tutorial.ML"

     4   "output_tutorial.ML"

     6   "antiquote_setup.ML"

     5   "antiquote_setup.ML"

     7 begin

     6 begin

     8 

     7 

     9 (* re-definition of various ML antiquotations    *)

     8 (* re-definition of various ML antiquotations    *)

    10 (* to have a special tag for text enclosed in ML *)

     9 (* to have a special tag for text enclosed in ML *)