A.thy:2:18: unfinished-proof: sorry leaves the goal unproved
A.thy:3:1: document-argument: text expects a text argument, as in text \<open>...\<close>
B.thy:2:1: document-argument: unexpected 'libcmd' after the text of text; a command of another session? pass its directory with -d
