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/Stream_Space.thy
changeset 75455 91c16c5ad3e9
parent 69260 0a9688695a1b 
--- a/src/HOL/Probability/Stream_Space.thy	Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Probability/Stream_Space.thy	Tue May 17 14:10:14 2022 +0100
@@ -493,7 +493,7 @@
     proof (safe intro!: sets_Sup_in_sets del: subsetI equalityI)
       fix i :: nat
       show "space (?V i) = space ?R"
-        using scylinder_streams by (subst space_measure_of) (auto simp: )
+        using scylinder_streams by (subst space_measure_of) auto
       { fix A assume "A \<in> G"
         then have "scylinder (space S) (replicate i (space S) @ [A]) = (\<lambda>s. s !! i) -` A \<inter> streams (space S)"
           by (induction i) (auto simp add: streams_shd streams_stl cong: conj_cong)
isabelle