Re: [isabelle] baffled by fun error message
On Tue, 22 Sep 2015, Thomas Sternagel wrote:
When I try the following minimal example in Isabelle2015
I get the error message:
exception THM 0 raised (line 744 of "thm.ML"):
forall_intr: variable "R" free in assumptions
wf R â
(âf ts x. x â set ts â (x, Fun f ts) â R) â
âx. Wellfounded.accp star_rel x
[star_rel â ??.Test.star_rel]
Which leaves me quite puzzled. I do neither understand the error
message nor why there is an error at all. Can somebody explain what
happens here, please?
It means that the function package is not fully localized, even though it
happens to be one of the first local theory packages in history.
I have refined that in Isabelle/ce74c00de6b7, so it should work better in
the coming release.
This archive was generated by a fusion of
Pipermail (Mailman edition) and