A suggestion and some compliments...
Larry
Begin forwarded message:
> From: James Frank
> 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 documen
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 me
