[isabelle-dev] Explicit option "open" for code_reflect

Frédéric Tuong frederic.tuong at lri.fr
Tue Oct 13 20:21:31 CEST 2015

Hi Florian,

Between Isabelle 2014 and 2015, the option "open" appeared for the 
command export_code, and by default the reflection minimizes the 
exported code.
Would it be acceptable for code_reflect to also have a similar option 

As a draft example, here is a list of modifications needed for 
implementing the option "open":
We basically abstract the parameter "false" of Code_Target.produce_code, 
and propagate this information to the parsing step.


More information about the isabelle-dev mailing list