[isabelle-dev] record: fold_congs/unfold_congs

[Michael Norrish]

On 18/04/12 1:46 PM, Thomas Sewell wrote:

> This is used in our modified version of the Schirmer Hoare VCG. I
> suppose that we've released the c-parser sources (which load extra
> fold_congs) but not the modified Hoare package (which uses them). The
> point is to avoid an exponential time/space explosion when updates of
> the form "% rec. rec (| x := rec x + 1 |)" are performed in sequence.
> (The problem is the repeated rec.)

The modified Hoare package *is* part of our released c-parser.  All this
will soon (I have the release candidate running already) be available
for use on top of isabelle2011-1 (at the moment, the released code only
runs on isabelle2009).

Michael

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 551 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120418/c78c58c4/attachment.sig>