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;
authorwenzelm
Sat, 05 Mar 2016 21:23:28 +0100
changeset 62523 5335e5c53312
parent 62522 d32c23d29968
child 62524 bf9a024ca238
tuned;
src/HOL/Isar_Examples/Cantor.thy file | annotate | diff | comparison | revisions
src/HOL/Isar_Examples/Drinker.thy file | annotate | diff | comparison | revisions 
--- 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" ..
--- 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
isabelle