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.
Tuned proof of choice_eq.
authorberghofe
Wed, 29 Oct 2003 11:50:26 +0100
changeset 14248 399a3290936c
parent 14247 cb32eb89bddd
child 14249 05382e257d95
Tuned proof of choice_eq.
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/HOL.thy	Wed Oct 29 01:17:06 2003 +0100
+++ b/src/HOL/HOL.thy	Wed Oct 29 11:50:26 2003 +0100
@@ -540,7 +540,6 @@
   apply (rule allI)
   apply (rule ex1I)
   apply (erule spec)
-  apply (rule ccontr)
   apply (erule_tac x = "%z. if z = x then y else f z" in allE)
   apply (erule impE)
   apply (rule allI)
isabelle