changeset 23394 | 474ff28210c0 |
parent 21404 | eb85850d3eb7 |
child 23463 | 9953ff53cc64 |
--- a/src/HOL/Unix/Unix.thy Thu Jun 14 23:04:36 2007 +0200 +++ b/src/HOL/Unix/Unix.thy Thu Jun 14 23:04:39 2007 +0200 @@ -591,7 +591,7 @@ assumes "root =xs\<Rightarrow> root'" and "\<exists>att dir. root = Env att dir" shows "\<exists>att dir. root' = Env att dir" - using transition_type_safe and prems + using transition_type_safe and assms proof (rule transitions_invariant) show "\<forall>x \<in> set xs. True" by blast qed