[isabelle] Does it mean busy or something else? (purple background)



Hi famous people,

While I had a short test on a topic, I came to this example, with which I don't know how to interpret the purple background colour I get on “by (simp add: atomize_all atomize_eq atomize_imp)” in the sample below (also as attached file):

    inductive f :: "'a list ⇒ bool"
      where f1: "f []"

    lemma "(⋀foo a. foo = f a) ⟹ f a"
      proof -
        assume h: "⋀foo a. foo = f a"
have "True = f a" using h by (simp add: atomize_all atomize_eq atomize_imp)
        thus ?thesis by simp
      qed

I'm accustomed to see this background colour when it's busy, like with Metis, typically for a short time. Here, I wonder what it means, the background remains, I can't imagine the Simplifier (which I wanted on purpose instead of Blast) running forever like this, and the goal seems to be solved.

--
“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

Attachment: Test.thy
Description: Binary data



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