diff -r a5368278a72c -r b7c0bf788f50 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Thu Aug 03 15:03:07 2006 +0200
+++ b/src/HOL/Unix/Unix.thy	Thu Aug 03 15:03:08 2006 +0200
@@ -221,7 +221,7 @@
 *}
 
 definition
-  "access root path uid perms \<equiv>
+  "access root path uid perms =
     (case lookup root path of
       None \<Rightarrow> None
     | Some file \<Rightarrow>
@@ -641,7 +641,7 @@
 *}
 
 definition
-  "can_exec root xs \<equiv> \<exists>root'. root =xs\<Rightarrow> root'"
+  "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
 
 lemma can_exec_nil: "can_exec root []"
   unfolding can_exec_def by (blast intro: transitions.intros)
@@ -858,7 +858,7 @@
 *}
 
 definition (in situation)
-  "invariant root path \<equiv>
+  "invariant root path =
     (\<exists>att dir.
       access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
       user\<^isub>1 \<noteq> owner att \<and>