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:
http://isabelle.in.tum.de/repos/isabelle/file/d52da3e7aa4c/src/HOL/Tools/record.ML#l334
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.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
