| changeset 22284 | 8d6d489f6ab3 |
| parent 22093 | 98e3e9f00192 |
| child 23219 | 87ad6e8a5f2c |
--- 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