[isabelle-dev] Towards release

[René Thiemann]

Thanks Alex,
the fixed version works again for IsaFoR

Am 20.09.2011 um 11:22 schrieb Alexander Krauss:

>>> partial_function(option) foo :: "nat list \<Rightarrow> unit option"
>>> where "foo x = foo x"
>>> 
>>> works, but
>>> 
>>> partial_function(option) foo :: "'a list \<Rightarrow> unit option"
>>> where "foo x = foo x"
>>> 
>>> yields the following error message.
>>> 
>>> *** exception THM 0 raised (line 1175 of "thm.ML"): instantiate: type
> 
> 
>> Alex seems to have fixed this issue with changeset 8b74cfea913a
> 
> Yes, many thanks for reporting this one. It came in when I added the generation of induction rules (which is still somewhat unfinished) in df41a5762c3d. This also shows that partial_function isn't terribly well-tested at the moment.
> 
> Alex
> 

-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck