Re: [isabelle] A few questions about Isabelle2013
On Sat, 12 Jan 2013, Gottfried Barrow wrote:
SMT PROOFS DON'T RUN THAT RAN BEFORE, AND SLEDGEHAMMER WAS FIRST HAVING
I saw on the developers list that SMT causes problems, so that answered my
question about whether I should use SMT proofs. The reason I had a couple is
because they were about 4 times faster than the metis proofs that were found.
You need to be more specific about the kind of problems you throw at
Sledgehammer wasn't working correctly at first. It wasn't updating the
output window. It was possibly related to me trying to run it on the
theorems that had the SMT proofs that didn't work anymore. At some
point, after trying different options on different theorems,
Sledgehammer started working.
Can you explain this further, beyond the "works for me state"? Was it
just confusion about slightly changed options and editor reactivity, or a
genuine problem to be isolated?
This archive was generated by a fusion of
Pipermail (Mailman edition) and