[isabelle-dev] record: fold_congs/unfold_congs

Makarius makarius at sketis.net
Tue Apr 17 16:37:30 CEST 2012

This is probably mainly relevant to NICTA users of the record package.

When doing some cleanup and performance tuning of the record package, I 
discovered the following mysterious fold_congs and unfold_congs: 

They appear to go back to the initial NICTA contribution 50406c4951d9. I 
have also seen traces of that feature in the L4.verified C parser tool 
that became publicly available recently.

Do these fold_congs/unfold_congs still have any purpose?  In the reachable 
set of Isabelle and AFP applications they don't, as far as I can see.  So 
it looks like a candidate for garbage collection on the sources.


More information about the isabelle-dev mailing list