1.1 --- a/src/HOL/Unix/Unix.thy	Fri Oct 13 22:30:29 2006 +0200
     1.2 +++ b/src/HOL/Unix/Unix.thy	Sat Oct 14 23:25:46 2006 +0200
     1.3 @@ -833,8 +833,9 @@
     1.4      and perms\<^isub>2_not_writable: "Writable \<notin> perms\<^isub>2"
     1.5    notes facts = user\<^isub>1_known user\<^isub>1_not_root users_neq
     1.6      perms\<^isub>1_writable perms\<^isub>2_not_writable
     1.7 +begin
     1.8  
     1.9 -definition (in situation)
    1.10 +definition
    1.11    "bogus =
    1.12       [Mkdir user\<^isub>1 perms\<^isub>1 [user\<^isub>1, name\<^isub>1],
    1.13        Mkdir user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2],
    1.14 @@ -857,7 +858,7 @@
    1.15    neither owned and nor writable by @{term user\<^isub>1}.
    1.16  *}
    1.17  
    1.18 -definition (in situation)
    1.19 +definition
    1.20    "invariant root path =
    1.21      (\<exists>att dir.
    1.22        access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
    1.23 @@ -896,7 +897,7 @@
    1.24    we just have to inspect rather special cases.
    1.25  *}
    1.26  
    1.27 -lemma (in situation) cannot_rmdir:
    1.28 +lemma cannot_rmdir:
    1.29    assumes inv: "invariant root bogus_path"
    1.30      and rmdir: "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
    1.31    shows False
    1.32 @@ -912,7 +913,7 @@
    1.33    ultimately show False by (simp add: bogus_path_def)
    1.34  qed
    1.35  
    1.36 -lemma (in situation)
    1.37 +lemma
    1.38    assumes init: "init users =bogus\<Rightarrow> root"
    1.39    notes eval = facts access_def init_def
    1.40    shows init_invariant: "invariant root bogus_path"
    1.41 @@ -935,7 +936,7 @@
    1.42    required here.
    1.43  *}
    1.44  
    1.45 -lemma (in situation) preserve_invariant:
    1.46 +lemma preserve_invariant:
    1.47    assumes tr: "root \<midarrow>x\<rightarrow> root'"
    1.48      and inv: "invariant root path"
    1.49      and uid: "uid_of x = user\<^isub>1"
    1.50 @@ -1079,7 +1080,7 @@
    1.51    overall procedure (see \secref{sec:unix-inv-procedure}).
    1.52  *}
    1.53  
    1.54 -corollary (in situation)
    1.55 +corollary
    1.56    assumes bogus: "init users =bogus\<Rightarrow> root"
    1.57    shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^isub>1) \<and>
    1.58      can_exec root (xs @ [Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1]]))"
    1.59 @@ -1089,3 +1090,5 @@
    1.60  qed
    1.61  
    1.62  end
    1.63 +
    1.64 +end