# HG changeset patch
# User wenzelm
# Date 1454757177 -3600
# Node ID f4baefee57768cf00b1a9e003770c7573b5d7378
# Parent  dfb70abaa3f07f70b70cb2e3c4f659b7f93ba278
tuned proofs;

diff -r dfb70abaa3f0 -r f4baefee5776 src/HOL/Isar_Examples/Cantor.thy
--- a/src/HOL/Isar_Examples/Cantor.thy	Fri Feb 05 10:21:38 2016 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy	Sat Feb 06 12:12:57 2016 +0100
@@ -71,6 +71,7 @@
   from * have "\<exists>x. ?D = f x" ..
   then obtain a where "?D = f a" ..
   then have "?D a \<longleftrightarrow> f a a" by (rule arg_cong)
+  then have "\<not> f a a \<longleftrightarrow> f a a" .
   then show False by (rule iff_contradiction)
 qed
 
diff -r dfb70abaa3f0 -r f4baefee5776 src/HOL/Isar_Examples/Higher_Order_Logic.thy
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Fri Feb 05 10:21:38 2016 +0100
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Sat Feb 06 12:12:57 2016 +0100
@@ -282,6 +282,7 @@
   from * have "\<exists>x. ?D = f x" ..
   then obtain a where "?D = f a" ..
   then have "?D a \<longleftrightarrow> f a a" using refl by (rule subst)
+  then have "\<not> f a a \<longleftrightarrow> f a a" .
   then show \<bottom> by (rule iff_contradiction)
 qed