# HG changeset patch
# User wenzelm
# Date 1003766317 -7200
# Node ID b46b1bdbe3f5e5600a50f50ddc385428e369773b
# Parent  a625de9ad62a3419e110dc9da8009b4324a6ca7e
corollary;

diff -r a625de9ad62a -r b46b1bdbe3f5 src/HOL/Unix/Unix.thy
--- 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]]))"