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/Unix/Unix.thy
changeset 11072 8f47967ecc80
parent 11004 af8008e4de96
child 11549 e7265e70fd7c 
--- a/src/HOL/Unix/Unix.thy	Mon Feb 05 20:33:50 2001 +0100
+++ b/src/HOL/Unix/Unix.thy	Mon Feb 05 20:34:05 2001 +0100
@@ -259,7 +259,7 @@
 proof -
   assume "path' \<parallel> path"
   then obtain y z xs ys zs where
-    "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs"
+      "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs"
     by (blast dest: parallel_decomp)
   hence "lookup (update path' opt root) path = lookup root path"
     by (blast intro: lookup_update_other)
isabelle