[isabelle-dev] Problem with transfer method

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Sep 27 21:16:57 CEST 2013


referring to 024fadbd03f0, at the end of the attached theory:

> context field_char_0
> begin
> lemma of_rat_minus: "of_rat (- a) = - of_rat a"
>   apply transfer

the »- _« (name uminus) gets replaced by a bound variable »uminusa«.
There seems to be a problem with the context here.

Sorry for not distilling a smaller example, but I have no idea how to
restore this situation after the final declarations

> lifting_update rat.lifting
> lifting_forget rat.lifting

in Rat.thy.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Transfer_Context.thy
Type: application/x-extension-thy
Size: 23252 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130927/b9f2797f/attachment-0001.bin>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 263 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130927/b9f2797f/attachment-0001.asc>

More information about the isabelle-dev mailing list