changeset 54147 | 97a8ff4e4ac9 |
parent 53820 | 9c7e97d67b45 |
child 54148 | c8cc5ab4a863 |
--- a/src/HOL/Finite_Set.thy Fri Oct 18 10:35:57 2013 +0200 +++ b/src/HOL/Finite_Set.thy Fri Oct 18 10:43:20 2013 +0200 @@ -1620,8 +1620,7 @@ show False by simp (blast dest: Suc_neq_Zero surjD) qed -(* Often leads to bogus ATP proofs because of reduced type information, hence no_atp *) -lemma infinite_UNIV_char_0 [no_atp]: +lemma infinite_UNIV_char_0: "\<not> finite (UNIV :: 'a::semiring_char_0 set)" proof assume "finite (UNIV :: 'a set)"