# HG changeset patch
# User wenzelm
# Date 1451748756 -3600
# Node ID 5651de00bca9504758adb8d3441948868638b974
# Parent  9bb80149dad9590766c5af578f58ceff907afe40
tuned;

diff -r 9bb80149dad9 -r 5651de00bca9 src/HOL/Isar_Examples/Cantor.thy
--- a/src/HOL/Isar_Examples/Cantor.thy	Sat Jan 02 16:15:28 2016 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy	Sat Jan 02 16:32:36 2016 +0100
@@ -17,7 +17,7 @@
   \<^item> @{url "https://en.wikipedia.org/wiki/Cantor's_diagonal_argument"}
 \<close>
 
-theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A :: 'a set. \<exists>x :: 'a. A = f x)"
+theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x)"
 proof
   assume "\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. A = f x"
   then obtain f :: "'a \<Rightarrow> 'a set" where *: "\<forall>A. \<exists>x. A = f x" ..
@@ -63,14 +63,14 @@
   with * show A ..
 qed
 
-theorem Cantor': "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A :: 'a \<Rightarrow> bool. \<exists>x :: 'a. A = f x)"
+theorem Cantor': "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x)"
 proof
-  assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A :: 'a \<Rightarrow> bool. \<exists>x. A = f x"
+  assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x"
   then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where *: "\<forall>A. \<exists>x. A = f x" ..
   let ?D = "\<lambda>x. \<not> f x x"
   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 "?D a \<longleftrightarrow> f a a" by (rule arg_cong)
   then show False by (rule iff_contradiction)
 qed
 
diff -r 9bb80149dad9 -r 5651de00bca9 src/HOL/Isar_Examples/Higher_Order_Logic.thy
--- a/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Sat Jan 02 16:15:28 2016 +0100
+++ b/src/HOL/Isar_Examples/Higher_Order_Logic.thy	Sat Jan 02 16:32:36 2016 +0100
@@ -274,7 +274,7 @@
   with * show A ..
 qed
 
-theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A :: 'a \<Rightarrow> o. \<exists>x :: 'a. A = f x)"
+theorem Cantor: "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x)"
 proof
   assume "\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> o. \<forall>A. \<exists>x. A = f x"
   then obtain f :: "'a \<Rightarrow> 'a \<Rightarrow> o" where *: "\<forall>A. \<exists>x. A = f x" ..