Thanks, that explains things.
Gerwin
On 05/10/2011, at 4:42 PM, Sascha Boehme wrote:
Hi Gerwin,
This is because by default the smt method tries to reconstruct the
proof of Z3. For bitvectors, however, there is currently no Z3 proof
reconstruction. You might want to invoke the smt method
A suggestion and some compliments...
Larry
Begin forwarded message:
From: James Frank s...@gmx.com
Subject: Needed ghostscript package to build PDF in Cygwin
Date: 5 October 2011 15:54:30 GMT+01:00
To: l...@cam.ac.uk
Dear Dr. Paulson,
The problem I had with building the Isabelle PDF
