3      Hoare_gen

     3      Hoare_gen

     4 

     4 

     5 session "Hoare_tm" in "thys" = "Hoare_gen" +

     5 session "Hoare_tm" in "thys" = "Hoare_gen" +

     6   theories 

     6   theories 

     7      Hoare_tm

     7      Hoare_tm

     8 

     9 

     9 session "Hoare_abc" in "thys" = "Hoare_tm" +

    10 session "Hoare_abc" in "thys" = "Hoare_tm" +

    10   theories

    11   theories

    11      Hoare_abc

    12      Hoare_abc

    12 

    14 

    13 session "TM" in "thys" = Hoare_abc +

    15 session "TM" in "thys" = Hoare_abc +

    14   theories 

    16   theories 

    15     My_block

    17     My_block

    16     LetElim

    18     LetElim

    18     StateMonad

    19     StateMonad

    19     TM_Assemble

    20     TM_Assemble

    20 

    21 

    21 session "Paper" in "paper" = TM +

    22 session "Paper" in "paper" = TM +

    22   options [document = pdf, document_output = "..", document_variants = "journal"]

    23   options [document = pdf, document_output = "..", document_variants = "journal"]