[isabelle-dev] record: fold_congs/unfold_congs
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