Email Gateway (Aug 19 2022 at 13:05): Email Gateway (Aug 19 2022 at 13:05):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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.
Test.thy
Last updated: Apr 26 2024 at 20:16 UTC