Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Adapted to changes in Finite_Set theory.
authorberghofe
Wed, 07 Feb 2007 18:12:02 +0100
changeset 22284 8d6d489f6ab3
parent 22283 26140713540b
child 22285 bbc76be6efb4
Adapted to changes in Finite_Set theory.
src/HOL/ex/Refute_Examples.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle