1 theory Base

     1 theory Base

     2 imports Main

     2 imports Main

     3 uses

     3 uses

     4   "chunks.ML"

     5   "chunks.ML"

     5   "antiquote_setup.ML"

     6   "antiquote_setup.ML"

     6 begin

     7 begin

     7 

     8 

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

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

    35   (OuterKeyword.tag "TutorialML" OuterKeyword.diag)

    36   (OuterKeyword.tag "TutorialML" OuterKeyword.diag)

    36     (OuterParse.ML_source >> IsarCmd.ml_diag true);

    37     (OuterParse.ML_source >> IsarCmd.ml_diag true);

    37 

    38 

    38 *}

    39 *}

    39 

    40 

    40 end

    42 end