Re: [isabelle-dev] AFP entry Grith_Chromatic fails with "THM 0"

2012-10-10 Thread Lukas Bulwahn
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

Re: [isabelle-dev] AFP entry Grith_Chromatic fails with "THM 0"

2012-10-10 Thread Makarius
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

[isabelle-dev] AFP entry Grith_Chromatic fails with "THM 0"

2012-10-10 Thread Johannes Hölzl
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