[isabelle-dev] Problem with transfer method

[Florian Haftmann]

Hi,

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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>