There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
No backend handles STRING
No backend is currently able to prove
LEMMA "a" \in STRING
The Isabelle backend has a definition of STRING, but the constant is currently called String, and no automation is set up for it. The other backends do not know about STRING.