| changeset 22093 | 98e3e9f00192 |
| parent 21985 | acfb13e8819e |
| child 22284 | 8d6d489f6ab3 |
--- a/src/HOL/ex/Refute_Examples.thy Fri Jan 19 21:20:10 2007 +0100 +++ b/src/HOL/ex/Refute_Examples.thy Fri Jan 19 22:04:22 2007 +0100 @@ -980,6 +980,10 @@ refute oops +lemma "x \<in> Finites" + refute -- {* no finite countermodel exists *} +oops + lemma "finite x" refute -- {* no finite countermodel exists *} oops