# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1468511362 -3600
# Node ID d51a0a772094bf71ca220dec4648d08966055a21
# Parent  a662e81398044af0cabdc15ca6e8c3c41c3530aa
Got rid of the \nexists macro

diff -r a662e8139804 -r d51a0a772094 src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Jul 14 14:48:49 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Thu Jul 14 16:49:22 2016 +0100
@@ -4114,9 +4114,9 @@
   have "~ ?rhs \<longleftrightarrow> ~ ?lhs"
   proof
     assume notr: "~ ?rhs"
-    have nog: "\<nexists>g. continuous_on (S \<union> connected_component_set (- S) a) g \<and>
+    have nog: "~ (\<exists>g. continuous_on (S \<union> connected_component_set (- S) a) g \<and>
                    g ` (S \<union> connected_component_set (- S) a) \<subseteq> sphere 0 1 \<and>
-                   (\<forall>x\<in>S. g x = (x - a) /\<^sub>R norm (x - a))"
+                   (\<forall>x\<in>S. g x = (x - a) /\<^sub>R norm (x - a)))"
          if "bounded (connected_component_set (- S) a)"
       apply (rule non_extensible_Borsuk_map [OF \<open>compact S\<close> componentsI _ aincc])
       using  \<open>a \<notin> S\<close> that by auto