[isabelle-dev] record: fold_congs/unfold_congs
Michael.Norrish at nicta.com.au
Wed Apr 18 06:15:25 CEST 2012
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).
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 551 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev