[isabelle] Performing global rewrites on the code setup



Dear list,

I am trying to apply a function "thm list -> thm list" to the global set
of code equations. I thought "functrans" allow me to do that, but
apparently they only work locally (i.e. on a single function). My use
case is to unfold all constants of arity zero.

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.