> 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. Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
