Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Probability/Discrete_Topology.thy
changeset 74362 0135a0c77b64
parent 69260 0a9688695a1b 
--- a/src/HOL/Probability/Discrete_Topology.thy	Fri Sep 24 13:40:14 2021 +0200
+++ b/src/HOL/Probability/Discrete_Topology.thy	Fri Sep 24 22:23:26 2021 +0200
@@ -32,10 +32,10 @@
 
 instance discrete :: (type) complete_space
 proof
-  fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X"
-  hence "\<exists>n. \<forall>m\<ge>n. X n = X m"
+  fix X::"nat\<Rightarrow>'a discrete"
+  assume "Cauchy X"
+  then obtain n where "\<forall>m\<ge>n. X n = X m"
     by (force simp: dist_discrete_def Cauchy_def split: if_split_asm dest:spec[where x=1])
-  then guess n ..
   thus "convergent X"
     by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n])
        (simp add: dist_discrete_def)
isabelle