# HG changeset patch
# User wenzelm
# Date 1457209408 -3600
# Node ID 5335e5c53312ddec63fe6dbb6bb84552a8493381
# Parent  d32c23d29968943c99734c0bab80bbf474ef096f
tuned;

diff -r d32c23d29968 -r 5335e5c53312 src/HOL/Isar_Examples/Cantor.thy
--- a/src/HOL/Isar_Examples/Cantor.thy	Sat Mar 05 20:47:31 2016 +0100
+++ b/src/HOL/Isar_Examples/Cantor.thy	Sat Mar 05 21:23:28 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. \<exists>x. A = f x)"
+theorem Cantor: "\<nexists>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" ..
@@ -35,10 +35,10 @@
   works.
 \<close>
 
-theorem "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A)"
+theorem "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A"
   by best
 
-theorem "\<not> (\<exists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A)"
+theorem "\<nexists>f :: 'a \<Rightarrow> 'a set. \<forall>A. \<exists>x. f x = A"
   by force
 
 
@@ -63,7 +63,7 @@
   with * show A ..
 qed
 
-theorem Cantor': "\<not> (\<exists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x)"
+theorem Cantor': "\<nexists>f :: 'a \<Rightarrow> 'a \<Rightarrow> bool. \<forall>A. \<exists>x. A = f x"
 proof
   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" ..
diff -r d32c23d29968 -r 5335e5c53312 src/HOL/Isar_Examples/Drinker.thy
--- a/src/HOL/Isar_Examples/Drinker.thy	Sat Mar 05 20:47:31 2016 +0100
+++ b/src/HOL/Isar_Examples/Drinker.thy	Sat Mar 05 21:23:28 2016 +0100
@@ -19,14 +19,14 @@
   assumes "\<not> (\<forall>x. P x)"
   shows "\<exists>x. \<not> P x"
 proof (rule classical)
-  assume "\<not> (\<exists>x. \<not> P x)"
+  assume "\<nexists>x. \<not> P x"
   have "\<forall>x. P x"
   proof
     fix x show "P x"
     proof (rule classical)
       assume "\<not> P x"
       then have "\<exists>x. \<not> P x" ..
-      with \<open>\<not> (\<exists>x. \<not> P x)\<close> show ?thesis by contradiction
+      with \<open>\<nexists>x. \<not> P x\<close> show ?thesis by contradiction
     qed
   qed
   with \<open>\<not> (\<forall>x. P x)\<close> show ?thesis by contradiction