session "Hoare_gen" in "thys" = "HOL" + theories Hoare_gen session "Hoare_tm" in "thys" = "Hoare_gen" + theories Hoare_tm session "Hoare_abc" in "thys" = "Hoare_tm" + theories Hoare_abc session "TM" in "thys" = Hoare_abc + theories TM_Assemble