Dear Leo,
Am 04.07.2014 um 07:48 schrieb Leo Freitas :
> Sledgehammering...
> "z3": The generated problem is malformed. Please report this to the Isabelle
> developers.
>
> I wasn’t sure whether the cast I was making for the shift operation was right
> or not, but anyhow I thought to send it
Hi Leo,
Am 04.07.2014 um 07:48 schrieb Leo Freitas :
> I was playing with HOL-Word to see if I could bring some discharged VCs from
> another tool into Isabelle.
> When I tried sledgehammer on it I got the error message for Z3
Thanks for the report! We will look into this. It may take some time
Hi,
I was playing with HOL-Word to see if I could bring some discharged VCs from
another tool into Isabelle.
When I tried sledgehammer on it I got the error message for Z3
theory Scratch
imports Main Word "~~/src/HOL/Word/WordBitwise"
begin
type_synonym word32 = "32 word"
lemma "(sint (True
