HomeIsabelle/Phabricator

clarified session: avoid merge of different syntax from different Hoare logics;