> I’m at home today so don’t have access to that file.

Please send it to me once you have a chance.

> But even if I somehow misspelt “yes” five times,

But maybe you wrote "true" five times?

> would it revert to “unknown”? 

Any value other than "yes" and "no" is taken as "unknown".

> Of course spaces should be ignored, esp. at the end.

I just copied old code I inherited from Sascha Böhm and his Vampire 
noncommercial. For sure there are endlessly many ways in which we could make 
Isabelle and Sledgehammer more user friendly. In Qt/C++, we had a 
"stripWhiteSpace" function that would do the trick. But string manipulation in 
ML is like pulling teeth. If you happen to know which function I can call, I'll 
gladly change the code.


isabelle-dev mailing list

Reply via email to