5 

     5 

     6 notation (latex output)

     6 notation (latex output)

     7   set ("_") and

     7   set ("_") and

     8   Cons  ("_::/_" [66,65] 65) 

     8   Cons  ("_::/_" [66,65] 65) 

     9 

     9 

    10 ML {*

    11 ML {*

    11   open Printer;

    12   open Printer;

    12   show_question_marks_default := false;

    13   show_question_marks_default := false;

    13   *}

    14   *}

    14 

    16 

    15 notation (latex output)

    17 notation (latex output)

    16   Cons ("_::_" [78,77] 73) and

    18   Cons ("_::_" [78,77] 73) and

    17   vt ("valid'_state") and

    19   vt ("valid'_state") and

    18   runing ("running") and

    20   runing ("running") and