It is probably due to my latest changeset in the
set_comprehension_pointfree simproc.
Lukas
On 10/10/2012 03:50 PM, Johannes Hölzl wrote:
Hi,
I tried to build AFP/Grith_Chormatic, but the simplifier fails in
Ugraphs.thy line 168:
using card_left_less_pair assms by simp
with the fo
On Wed, 10 Oct 2012, Johannes Hölzl wrote:
I tried to build AFP/Grith_Chormatic, but the simplifier fails in
Ugraphs.thy line 168:
using card_left_less_pair assms by simp
with the following exception:
exception THM 0 raised (line 790 of "drule.ML"):
Ill-typed instantiation:
Type
?'a
Hi,
I tried to build AFP/Grith_Chormatic, but the simplifier fails in
Ugraphs.thy line 168:
using card_left_less_pair assms by simp
with the following exception:
exception THM 0 raised (line 790 of "drule.ML"):
Ill-typed instantiation:
Type
?'a ⇒ ?'b
of variable ?f
cannot be