corollary;

--- a/src/HOL/Unix/Unix.thy	Mon Oct 22 17:58:26 2001 +0200
+++ b/src/HOL/Unix/Unix.thy	Mon Oct 22 17:58:37 2001 +0200
@@ -1121,7 +1121,7 @@
   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]]))"