@liamoc The person next to me last year had difficulties with typing isabelle syntaxes on her computer. It did not help when her input method decided to enter symbols used in Chinese instead of ascii symbols. I guess we could teach people Holbert-ng next time when Holbert-ng is more mature
