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 23463 9953ff53cc64
parent 23394 474ff28210c0
child 23769 7bc32680a495 
--- a/src/HOL/Unix/Unix.thy	Thu Jun 21 17:28:50 2007 +0200
+++ b/src/HOL/Unix/Unix.thy	Thu Jun 21 17:28:53 2007 +0200
@@ -570,7 +570,7 @@
   using trans
 proof induct
   case nil
-  show ?case by assumption
+  show ?case by (rule nil.prems)
 next
   case (cons root x root' xs root'')
   note P = `\<forall>x \<in> set (x # xs). P x`
isabelle