--- 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
--- 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