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`