src/HOL/Unix/Unix.thy

   The main result is now imminent, just by composing the three
   invariance lemmas (see \secref{sec:unix-inv-lemmas}) according the the
   overall procedure (see \secref{sec:unix-inv-procedure}).
 *}
 
-theorem main:
+corollary
   "init users =bogus\<Rightarrow> root \<Longrightarrow>
   \<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user1) \<and>
       can_exec root (xs @ [Rmdir user1 [user1, name1]]))"
 proof -
   case rule_context