OK, now I know the answer.
I opened Tobias's theories in HOL/IMP (because they use lift_definition)
and this actually imports HOL/ex/Interpretation_with_Defs.thy that
changes the global state (locale interpretations).
Tricky, but it makes sense.
Ondrej
On 05/15/2013 10:52 AM, Ondřej Kunčar wrote:
This refers to 68c163598f07 + my local patches in Lifting/Transfer.
During testing my local patches, I found out that I broke the theory
FinFun.thy
In every interpretation I got an error message "Illegal free variables
in expression: ...". For example for the first interpretation, it was
"b'". I don't think the error was related to my local changes since I
didn't change anything in locales and even if I did something strange
with contexts in lift_definition, it should be ok when we are back at
the toplevel.
I "fixed" the problem by writing "for b'" (for g and so on) for each
interpretation. But funnily after I restarted Jedit, I cannot reproduce
this problem any more, i.e, FinFun goes through even without these "for
b'" additional statements.
Another strange thing that might or might not be related: when I
hovered over b' in this expression
interpretation finfun_update: comp_fun_commute "λa f. f(a :: 'a $:= b')"
I got originally(=in the state with the error message mentioned above)
this type:
free variable
:: 'b
But now I get this:
free variable
:: 'b
:: 'b
(i.e., 'b is there twice)
Since I cannot reproduce this problem any more, might be hard to say
anything about it, but maybe it rings a bell in somebody's head.
Ondrej
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
