| changeset 76447 | 391b8db24c66 |
| parent 76422 | 2612b3406b61 |
| child 77695 | 93531ba2c784 |
--- a/src/HOL/Finite_Set.thy Fri Nov 04 20:56:07 2022 +0100 +++ b/src/HOL/Finite_Set.thy Sat Nov 05 09:57:51 2022 +0100 @@ -222,6 +222,9 @@ in proc end \<close> +(* Needs to be used with care *) +declare [[simproc del: finite]] + lemma finite_UnI: assumes "finite F" and "finite G" shows "finite (F \<union> G)"