Qiyuan Xu (Nov 26 2021 at 02:11): Qiyuan Xu (Nov 26 2021 at 02:11):In src/Pure/asssumption.ML, the ML type Assumption.export is defined as bool -> cterm list -> (thm -> thm) * (term -> term). The documentation implementation describes that type as however bool -> cterm list -> thm -> thm (page 121 for version Isabelle2021), which loses the explanation about the second argument, the export map of type term -> term. I guess it is used for exporting some term shape, but what term it is, the term of proposition of the theorem or the term variables (fixed variables)? However, both the standard exports, the assume_export and presume_export set that term export as just fn x => x, seeming that the term export just useless, which makes me confused more. While that term export, I found, does be used somewhere in the Isabelle system, can I naively set it also as fn x => x?
Qiyuan Xu (Nov 26 2021 at 02:18):When I set that as the naive fn x => x, everything works well, but it may just seem to work well...
Last updated: Jul 15 2022 at 23:21 UTC