> On 3 Jul 2018, at 13:07, Lawrence Paulson wrote:
>
> I keep getting the error message below. I have changed this option many times
> but it never sticks. It has been happening consistently since yesterday.
>
> ~/isabelle/Repos/src/HOL: hg id
> ec4fe1032b6e tip
Could it be something as simple
> 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
Well, there’s this:
> String.translate (fn c => if Char.isSpace c then "" else str c) " y e s
> ";
val it = "yes": string
No idea what Isabelle/ML does to these primitives however.
Larry
> On 4 Jul 2018, at 11:11, Blanchette, J.C. wrote:
>
> I just copied old code I inherited from Sasch
On 04/07/18 12:18, Lawrence Paulson wrote:
> Well, there’s this:
>
>> String.translate (fn c => if Char.isSpace c then "" else str c) " y e s
>> ";
> val it = "yes": string
>
> No idea what Isabelle/ML does to these primitives however.
This SML'97 stuff is indeed alien to Isabelle/ML, and
On 04/07/18 12:11, Blanchette, J.C. wrote:
>
> I just copied old code I inherited from Sascha Böhm and his Vampire
> noncommercial.
I only vaguely remember when we introduced the original non-commercial
settings variable for Z3, even with some insider joke about Microsoft:
changing the value req
Makarius wrote:
> I don't remember the reason for its "tristate logic", with "unknown" as
> default.
The thinking is as follows. In an "unknown" state, "vampire" gets added to the
list of provers by Sledgehammer, and users get a warning. In a "no" state, it
doesn't. Thus, "unknown" serves a do
