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.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.