| changeset 69144 | f13b82281715 |
| parent 68188 | 2af1f142f855 |
| child 73346 | 00e0f7724c06 |
--- a/src/HOL/Metis_Examples/Tarski.thy Wed Oct 17 07:50:46 2018 +0200 +++ b/src/HOL/Metis_Examples/Tarski.thy Wed Oct 17 14:19:07 2018 +0100 @@ -436,7 +436,7 @@ subsection \<open>fixed points\<close> lemma fix_subset: "fix f A \<subseteq> A" -by (simp add: fix_def, fast) +by (auto simp add: fix_def) lemma fix_imp_eq: "x \<in> fix f A ==> f x = x" by (simp add: fix_def)