Email Gateway (Nov 27 2021 at 09:14): Email Gateway (Nov 27 2021 at 09:14):From: Qiyuan Xu <xqyww123@gmail.com>
In src/Pure/asssumption.ML, the ML type Assumption.export is
defined as bool
-> cterm list -> (thm -> thm) * (term -> term). The implementation
documentation
describes that as however of type 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)? What it should be when
I setting the assumption export?
Last updated: Jul 15 2022 at 23:21 UTC