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`

?

When I set that as the naive `fn x => x`

, everything works well, but it may just seem to work well...

I have only used Assumption.import and co (the difference is that they work on a proper proof context), but my guess is that this comes from variables you declare locally (the one that become `?x`

in the goal) that can conflict with global constants.

It's a good idea to ask such questions on the mailing list, since the best person to answer them is probably Makarius, and he boycotts Zulip.

Mathias Fleury said:

I have only used Assumption.import and co (the difference is that they work on a proper proof context), but my guess is that this comes from variables you declare locally (the one that become

`?x`

in the goal) that can conflict with global constants.

sorry, do you mean the `import`

function in `Assumption`

structure? I don't find that function in file `src/Pure/assumption.ML`

Sorry I meant `Assumption.add_assumes`

Last updated: Dec 07 2023 at 16:21 UTC