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 qedI'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.”  “Structured Programming supports the law of the excluded muddle.”  : Epigrams on Programming — Alan J. — P. Yale University
Description: Binary data