# HG changeset patch
# User berghofe
# Date 1170868322 -3600
# Node ID 8d6d489f6ab36dc8e31cad45a37f99c5d19227ed
# Parent  26140713540b69e9f05b096815caef12791fdbbf
Adapted to changes in Finite_Set theory.

diff -r 26140713540b -r 8d6d489f6ab3 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Wed Feb 07 18:11:27 2007 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Wed Feb 07 18:12:02 2007 +0100
@@ -980,10 +980,6 @@
   refute
 oops
 
-lemma "x \<in> Finites"
-  refute  -- {* no finite countermodel exists *}
-oops
-
 lemma "finite x"
   refute  -- {* no finite countermodel exists *}
 oops